Nuprl Lemma : presheaf-elements-sq
∀C:SmallCategory. ∀P:Top.
(el(P) ~ Cat(ob = A:cat-ob(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(C) (fst(Aa));
comp(Aa,Bb,Dd,f,g) = cat-comp(C) (fst(Aa)) (fst(Bb)) (fst(Dd)) f g))
Proof
Definitions occuring in Statement :
presheaf-elements: el(P),
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),
small-category: SmallCategory,
top: Top,
pi1: fst(t),
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
spread: spread def,
product: x:A × B[x],
sqequal: s ~ t,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
small-category: SmallCategory,
op-cat: op-cat(C),
presheaf-elements: el(P),
member: t ∈ T,
top: Top,
spreadn: spread4
Lemmas referenced :
cat_ob_pair_lemma,
cat_id_tuple_lemma,
cat_comp_tuple_lemma,
cat_arrow_triple_lemma,
top_wf,
small-category_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalHypSubstitution,
setElimination,
thin,
rename,
productElimination,
sqequalRule,
introduction,
extract_by_obid,
dependent_functionElimination,
isect_memberEquality,
voidElimination,
voidEquality,
hypothesis
Latex:
\mforall{}C:SmallCategory. \mforall{}P:Top.
(el(P) \msim{} Cat(ob = A:cat-ob(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(C) (fst(Aa));
comp(Aa,Bb,Dd,f,g) = cat-comp(C) (fst(Aa)) (fst(Bb)) (fst(Dd)) f g))
Date html generated:
2020_05_20-AM-07_57_04
Last ObjectModification:
2017_10_03-AM-11_09_01
Theory : small!categories
Home
Index