Nuprl Definition : refl-contraction

refl-contraction(X;A;a) == singleton-contraction(X;refl(a))

Definitions occuring in Statement : singleton-contraction: singleton-contraction(X;pth), cubical-refl: refl(a)
Definitions occuring in definition : singleton-contraction: singleton-contraction(X;pth), cubical-refl: refl(a)
FDL editor aliases : refl-contraction

Latex:
refl-contraction(X;A;a) == singleton-contraction(X;refl(a)) Date html generated: 2018_05_23-AM-09_46_16 Last ObjectModification: 2017_11_07-PM-03_25_00 Theory : cubical!type!theory Home Index