Nuprl Definition : presheaf-type-iso
presheaf-type-iso(X) ==  λF.<λI,rho. (F <I, rho>), λI,J,f,a. (F <I, a> <J, f(a)> f)>
Definitions occuring in Statement : 
psc-restriction: f(s)
, 
functor-arrow: arrow(F)
, 
functor-ob: ob(F)
, 
apply: f a
, 
lambda: λx.A[x]
, 
pair: <a, b>
Definitions occuring in definition : 
functor-ob: ob(F)
, 
lambda: λx.A[x]
, 
apply: f a
, 
functor-arrow: arrow(F)
, 
pair: <a, b>
, 
psc-restriction: f(s)
FDL editor aliases : 
presheaf-type-iso
Latex:
presheaf-type-iso(X)  ==    \mlambda{}F.<\mlambda{}I,rho.  (F  <I,  rho>),  \mlambda{}I,J,f,a.  (F  <I,  a>  <J,  f(a)>  f)>
Date html generated:
2018_05_22-PM-10_01_49
Last ObjectModification:
2018_02_20-PM-03_04_05
Theory : presheaf!models!of!type!theory
Home
Index