Nuprl Definition : cubical-interval-filler

cubical-interval-filler() ==  λI,J,x,i,bx. if null(J) then cube(hd(bx)) else λL.cube(get_face(hd(J);L hd(J);bx))(L) fi 


Definitions occuring in Statement :  cubical-interval-ap: u(L),  get_face: get_face(y;c;box),  face-cube: cube(f),  hd: hd(l),  null: null(as),  ifthenelse: if b then t else f fi ,  apply: f a,  lambda: λx.A[x]
Definitions occuring in definition :  ifthenelse: if b then t else f fi ,  null: null(as),  lambda: λx.A[x],  cubical-interval-ap: u(L),  face-cube: cube(f),  get_face: get_face(y;c;box),  apply: f a,  hd: hd(l)
FDL editor aliases :  cubical-interval-filler
Latex:
cubical-interval-filler()  ==
    \mlambda{}I,J,x,i,bx.  if  null(J)  then  cube(hd(bx))  else  \mlambda{}L.cube(get\_face(hd(J);L  hd(J);bx))(L)  fi 


Date html generated: 2016_06_16-PM-06_50_25
Last ObjectModification: 2015_09_23-AM-09_32_48

Theory : cubical!sets


Home Index