Nuprl Definition : presheaf-subset
F|I,rho.P[I; rho] == Presheaf(Set(I) ={rho:F I| P[I; rho]} ;Morphism(I,J,f,rho) = F I J f rho)
Definitions occuring in Statement :
mk-presheaf: mk-presheaf,
functor-arrow: arrow(F),
functor-ob: ob(F),
set: {x:A| B[x]} ,
apply: f a
Definitions occuring in definition :
mk-presheaf: mk-presheaf,
set: {x:A| B[x]} ,
functor-ob: ob(F),
apply: f a,
functor-arrow: arrow(F)
FDL editor aliases :
presheaf-subset
Latex:
F|I,rho.P[I; rho] == Presheaf(Set(I) =\{rho:F I| P[I; rho]\} ;Morphism(I,J,f,rho) = F I J f rho)
Date html generated:
2020_05_20-AM-07_57_25
Last ObjectModification:
2017_10_03-PM-03_13_40
Theory : small!categories
Home
Index