Nuprl Definition : cubical-isect-elim
cubical-isect-elim(t) == λI,a. (t I (fst(a)) I 1)
Definitions occuring in Statement :
nh-id: 1,
pi1: fst(t),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
nh-id: 1,
pi1: fst(t),
apply: f a,
lambda: λx.A[x]
FDL editor aliases :
cubical-isect-elim
Latex:
cubical-isect-elim(t) == \mlambda{}I,a. (t I (fst(a)) I 1)
Date html generated:
2016_10_28-AM-11_16_52
Last ObjectModification:
2016_07_21-PM-00_33_09
Theory : cubical!type!theory
Home
Index