Nuprl Definition : nerve-box-common-face
nerve-box-common-face(box;L;z) ==
hd(filter(λf.((direction(f) =z L dimension(f)) ∧b (direction(f) =z flip(L;z) dimension(f)));box))
Definitions occuring in Statement :
face-direction: direction(f)
,
face-dimension: dimension(f)
,
name-morph-flip: flip(f;y)
,
hd: hd(l)
,
filter: filter(P;l)
,
band: p ∧b q
,
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]
,
band: p ∧b q
,
eq_int: (i =z j)
,
face-direction: direction(f)
,
apply: f a
,
name-morph-flip: flip(f;y)
,
face-dimension: dimension(f)
FDL editor aliases :
nerve-box-common-face
Latex:
nerve-box-common-face(box;L;z) ==
hd(filter(\mlambda{}f.((direction(f) =\msubz{} L dimension(f)) \mwedge{}\msubb{} (direction(f) =\msubz{} flip(L;z) dimension(f)));box))
Date html generated:
2016_06_16-PM-07_02_28
Last ObjectModification:
2015_09_23-AM-09_33_22
Theory : cubical!sets
Home
Index