Nuprl Definition : presheaf-elements
el(P) ==
Cat(ob = A:cat-ob(op-cat(C)) × (P A);
arrow(Aa,Bb) = let A,a = Aa
in let B,b = Bb
in {f:cat-arrow(op-cat(C)) B A| (P B A f b) = a ∈ (P A)} ;
id(Aa) = cat-id(op-cat(C)) (fst(Aa));
comp(Aa,Bb,Dd,f,g) = cat-comp(op-cat(C)) (fst(Dd)) (fst(Bb)) (fst(Aa)) g f)
Definitions occuring in Statement :
op-cat: op-cat(C),
functor-arrow: arrow(F),
functor-ob: ob(F),
mk-cat: mk-cat,
cat-comp: cat-comp(C),
cat-id: cat-id(C),
cat-arrow: cat-arrow(C),
cat-ob: cat-ob(C),
pi1: fst(t),
set: {x:A| B[x]} ,
apply: f a,
spread: spread def,
product: x:A × B[x],
equal: s = t ∈ T
Definitions occuring in definition :
mk-cat: mk-cat,
product: x:A × B[x],
cat-ob: cat-ob(C),
spread: spread def,
set: {x:A| B[x]} ,
cat-arrow: cat-arrow(C),
equal: s = t ∈ T,
functor-ob: ob(F),
functor-arrow: arrow(F),
cat-id: cat-id(C),
apply: f a,
cat-comp: cat-comp(C),
op-cat: op-cat(C),
pi1: fst(t)
FDL editor aliases :
presheaf-elements
Latex:
el(P) ==
Cat(ob = A:cat-ob(op-cat(C)) \mtimes{} (P A);
arrow(Aa,Bb) = let A,a = Aa
in let B,b = Bb
in \{f:cat-arrow(op-cat(C)) B A| (P B A f b) = a\} ;
id(Aa) = cat-id(op-cat(C)) (fst(Aa));
comp(Aa,Bb,Dd,f,g) = cat-comp(op-cat(C)) (fst(Dd)) (fst(Bb)) (fst(Aa)) g f)
Date html generated:
2020_05_20-AM-07_57_01
Last ObjectModification:
2017_10_03-AM-11_03_28
Theory : small!categories
Home
Index