Nuprl Definition : A-face-image
A-face-image(X;A;I;K;f;alpha;face) == let x,b,w = face in <f x, b, (w (x:=b)(alpha) f)>
Definitions occuring in Statement :
cubical-type-ap-morph: (u a f),
cube-set-restriction: f(s),
face-map: (x:=i),
cname_deq: CnameDeq,
list-diff: as-bs,
cons: [a / b],
nil: [],
spreadn: spread3,
apply: f a,
pair: <a, b>
Definitions occuring in definition :
spreadn: spread3,
pair: <a, b>,
cubical-type-ap-morph: (u a f),
apply: f a,
cube-set-restriction: f(s),
list-diff: as-bs,
cname_deq: CnameDeq,
cons: [a / b],
nil: [],
face-map: (x:=i)
FDL editor aliases :
A-face-image
Latex:
A-face-image(X;A;I;K;f;alpha;face) == let x,b,w = face in <f x, b, (w (x:=b)(alpha) f)>
Date html generated:
2016_06_16-PM-05_51_20
Last ObjectModification:
2015_09_23-AM-09_31_39
Theory : cubical!sets
Home
Index