Nuprl Definition : nerve-box-face
nerve-box-face(box;L) == hd(filter(λf.(direction(f) =z L dimension(f));box))
Definitions occuring in Statement :
face-direction: direction(f),
face-dimension: dimension(f),
hd: hd(l),
filter: filter(P;l),
eq_int: (i =z j),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
hd: hd(l),
filter: filter(P;l),
lambda: λx.A[x],
eq_int: (i =z j),
face-direction: direction(f),
apply: f a,
face-dimension: dimension(f)
FDL editor aliases :
nerve-box-face
Latex:
nerve-box-face(box;L) == hd(filter(\mlambda{}f.(direction(f) =\msubz{} L dimension(f));box))
Date html generated:
2016_06_16-PM-07_02_13
Last ObjectModification:
2015_09_23-AM-09_33_19
Theory : cubical!sets
Home
Index