Nuprl Lemma : presheaf-elements-sq

`∀C:SmallCategory. ∀P:Top.`
`  (el(P) ~ Cat(ob = A:cat-ob(C) × (ob(P) A);`
`               arrow(Aa,Bb) = let A,a = Aa `
`                              in let B,b = Bb `
`                                 in {f:cat-arrow(op-cat(C)) B A| (arrow(P) B A f b) = a ∈ (ob(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{}  (ob(P)  A);
arrow(Aa,Bb)  =  let  A,a  =  Aa
in  let  B,b  =  Bb
in  \{f:cat-arrow(op-cat(C))  B  A|  (arrow(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: 2017_10_05-AM-00_50_40
Last ObjectModification: 2017_10_03-AM-11_09_01

Theory : small!categories

Home Index