Nuprl Definition : term-A-face
This makes a <y,i>-face (where y is fresh(I)) that is equal to the
given cubical term, a.⋅
term-A-face(a;I;alpha;i) == <fresh-cname(I), i, a(alpha)>
Definitions occuring in Statement :
cubical-term-at: u(a),
fresh-cname: fresh-cname(I),
pair: <a, b>
Definitions occuring in definition :
fresh-cname: fresh-cname(I),
pair: <a, b>,
cubical-term-at: u(a)
FDL editor aliases :
term-A-face
Latex:
term-A-face(a;I;alpha;i) == <fresh-cname(I), i, a(alpha)>
Date html generated:
2016_07_08-PM-10_40_09
Last ObjectModification:
2015_09_23-AM-09_34_37
Theory : cubical!sets
Home
Index