Nuprl Definition : get_face
get_face(y;c;box) == hd(filter(λf.((fst(f) =z y) ∧b (fst(snd(f)) =z c));box))
Definitions occuring in Statement :
hd: hd(l),
filter: filter(P;l),
band: p ∧b q,
eq_int: (i =z j),
pi1: fst(t),
pi2: snd(t),
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),
pi1: fst(t),
pi2: snd(t)
FDL editor aliases :
get_face
Latex:
get\_face(y;c;box) == hd(filter(\mlambda{}f.((fst(f) =\msubz{} y) \mwedge{}\msubb{} (fst(snd(f)) =\msubz{} c));box))
Date html generated:
2016_06_16-PM-05_55_23
Last ObjectModification:
2015_09_23-AM-09_31_44
Theory : cubical!sets
Home
Index