Nuprl Definition : face-one
(i=1) == λI,rho. dM-to-FL(I;i(rho))
Definitions occuring in Statement :
cubical-term-at: u(a),
dM-to-FL: dM-to-FL(I;z),
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
dM-to-FL: dM-to-FL(I;z),
cubical-term-at: u(a)
FDL editor aliases :
face-one
Latex:
(i=1) == \mlambda{}I,rho. dM-to-FL(I;i(rho))
Date html generated:
2016_05_19-AM-08_26_19
Last ObjectModification:
2016_03_03-PM-08_04_59
Theory : cubical!type!theory
Home
Index