Nuprl Definition : presheaf-subset
F|I,rho.P[I; rho] == Presheaf(Set(I) ={rho:ob(F) I| P[I; rho]} ;Morphism(I,J,f,rho) = arrow(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 :
functor-arrow: arrow(F),
apply: f a,
functor-ob: ob(F),
set: {x:A| B[x]} ,
mk-presheaf: mk-presheaf
FDL editor aliases :
presheaf-subset
Latex:
F|I,rho.P[I; rho] == Presheaf(Set(I) =\{rho:ob(F) I| P[I; rho]\} ;Morphism(I,J,f,rho) = arrow(F) I J \000Cf rho)
Date html generated:
2017_10_05-AM-00_50_57
Last ObjectModification:
2017_10_03-PM-03_13_40
Theory : small!categories
Home
Index