Nuprl Definition : cubical-type-rev-iso
cubical-type-rev-iso(X) ==
λF.Presheaf(Set(p) =(fst(F)) (fst(p)) (snd(p));
Morphism(p,q,f,a) = (snd(F)) (fst(p)) (fst(q)) f (snd(p)) a)
Definitions occuring in Statement :
mk-presheaf: mk-presheaf,
pi1: fst(t),
pi2: snd(t),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
pi2: snd(t),
pi1: fst(t),
apply: f a,
mk-presheaf: mk-presheaf,
lambda: λx.A[x]
FDL editor aliases :
cubical-type-rev-iso
Latex:
cubical-type-rev-iso(X) ==
\mlambda{}F.Presheaf(Set(p) =(fst(F)) (fst(p)) (snd(p));
Morphism(p,q,f,a) = (snd(F)) (fst(p)) (fst(q)) f (snd(p)) a)
Date html generated:
2017_10_05-AM-01_21_09
Last ObjectModification:
2017_10_04-PM-01_09_41
Theory : cubical!type!theory
Home
Index