Nuprl Definition : lift-id-faces
lift-id-faces(X;A;I;alpha;box) == map(λface.lift-id-face(X;A;I;alpha;face);box)
Definitions occuring in Statement :
lift-id-face: lift-id-face(X;A;I;alpha;face),
map: map(f;as),
lambda: λx.A[x]
Definitions occuring in definition :
map: map(f;as),
lambda: λx.A[x],
lift-id-face: lift-id-face(X;A;I;alpha;face)
FDL editor aliases :
lift-id-faces
Latex:
lift-id-faces(X;A;I;alpha;box) == map(\mlambda{}face.lift-id-face(X;A;I;alpha;face);box)
Date html generated:
2016_06_16-PM-07_32_47
Last ObjectModification:
2015_09_23-AM-09_34_33
Theory : cubical!sets
Home
Index