Nuprl Definition : presheaf-type-rev-iso

presheaf-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 :  lambda: λx.A[x],  mk-presheaf: mk-presheaf,  apply: f a,  pi1: fst(t),  pi2: snd(t)
FDL editor aliases :  presheaf-type-rev-iso
Latex:
presheaf-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: 2018_05_22-PM-10_02_02
Last ObjectModification: 2018_02_20-PM-03_04_15

Theory : presheaf!models!of!type!theory


Home Index