Nuprl Definition : nerve_box_edge
nerve_box_edge(box;c;y) ==  functor-arrow(cube(nerve-box-common-face(box;c;y))) c flip(c;y) (λx.Ax)
Definitions occuring in Statement : 
nerve-box-common-face: nerve-box-common-face(box;L;z)
, 
face-cube: cube(f)
, 
name-morph-flip: flip(f;y)
, 
functor-arrow: functor-arrow(F)
, 
apply: f a
, 
lambda: λx.A[x]
, 
axiom: Ax
Definitions occuring in definition : 
apply: f a
, 
functor-arrow: functor-arrow(F)
, 
face-cube: cube(f)
, 
nerve-box-common-face: nerve-box-common-face(box;L;z)
, 
name-morph-flip: flip(f;y)
, 
lambda: λx.A[x]
, 
axiom: Ax
FDL editor aliases : 
nerve_box_edge
Latex:
nerve\_box\_edge(box;c;y)  ==    functor-arrow(cube(nerve-box-common-face(box;c;y)))  c  flip(c;y)  (\mlambda{}x.Ax)
Date html generated:
2016_06_16-PM-07_04_01
Last ObjectModification:
2015_09_23-AM-09_33_28
Theory : cubical!sets
Home
Index