Nuprl Definition : lift-id-face
lift-id-face(X;A;I;alpha;face) ==
let y,c,w = face in
<y, c, snd(set-path-name(X;A;I-[y];(y:=c)(alpha);fresh-cname(I);w))>
Definitions occuring in Statement :
set-path-name: set-path-name(X;A;I;alpha;x;p),
cube-set-restriction: f(s),
face-map: (x:=i),
fresh-cname: fresh-cname(I),
cname_deq: CnameDeq,
list-diff: as-bs,
cons: [a / b],
nil: [],
spreadn: spread3,
pi2: snd(t),
pair: <a, b>
Definitions occuring in definition :
spreadn: spread3,
pair: <a, b>,
pi2: snd(t),
set-path-name: set-path-name(X;A;I;alpha;x;p),
cube-set-restriction: f(s),
list-diff: as-bs,
cname_deq: CnameDeq,
cons: [a / b],
nil: [],
face-map: (x:=i),
fresh-cname: fresh-cname(I)
FDL editor aliases :
lift-id-face
Latex:
lift-id-face(X;A;I;alpha;face) ==
let y,c,w = face in
<y, c, snd(set-path-name(X;A;I-[y];(y:=c)(alpha);fresh-cname(I);w))>
Date html generated:
2016_06_16-PM-07_32_28
Last ObjectModification:
2015_09_23-AM-09_34_30
Theory : cubical!sets
Home
Index