Nuprl Definition : refl-map
refl-map(X;A) == cubical-lam(X;discr(refl(q)))
Definitions occuring in Statement :
cubical-refl: refl(a),
discrete-cubical-term: discr(t),
cubical-lam: cubical-lam(X;b),
cc-snd: q,
cube-context-adjoin: X.A
Definitions occuring in definition :
cc-snd: q,
cube-context-adjoin: X.A,
cubical-refl: refl(a),
discrete-cubical-term: discr(t),
cubical-lam: cubical-lam(X;b)
FDL editor aliases :
refl-map
Latex:
refl-map(X;A) == cubical-lam(X;discr(refl(q)))
Date html generated:
2017_02_21-AM-10_53_37
Last ObjectModification:
2017_02_20-PM-11_10_00
Theory : cubical!type!theory
Home
Index