Nuprl Definition : face-zero
(i=0) == λ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),
names-deq: NamesDeq,
names: names(I),
dm-neg: ¬(x),
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
dM-to-FL: dM-to-FL(I;z),
dm-neg: ¬(x),
names: names(I),
names-deq: NamesDeq,
cubical-term-at: u(a)
FDL editor aliases :
face-zero
Latex:
(i=0) == \mlambda{}I,rho. dM-to-FL(I;\mneg{}(i(rho)))
Date html generated:
2016_05_19-AM-08_26_30
Last ObjectModification:
2016_03_03-PM-07_56_34
Theory : cubical!type!theory
Home
Index