Nuprl Definition : cubical-refl
refl(a) == λI,alpha. refl-path(A;a;I;alpha)
Wellformedness Lemmas :
cubical-refl_wf
Definitions occuring in Statement :
refl-path: refl-path(A;a;I;alpha),
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
refl-path: refl-path(A;a;I;alpha)
FDL editor aliases :
cubical-refl
cubical-refl
cubical-refl
Latex:
refl(a) == \mlambda{}I,alpha. refl-path(A;a;I;alpha)
Date html generated:
2016_06_16-PM-08_06_21
Last ObjectModification:
2015_09_23-AM-09_34_55
Theory : cubical!sets
Home
Index