Nuprl Lemma : sets-ob

[C:SmallCategory]. ∀[X:Top].  (cat-ob(sets(C; X)) I:cat-ob(C) × X(I))


Proof




Definitions occuring in Statement :  sets: sets(C; X) I_set: A(I) cat-ob: cat-ob(C) small-category: SmallCategory uall: [x:A]. B[x] top: Top product: x:A × B[x] sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T small-category: SmallCategory spreadn: spread4 I_set: A(I) sets: sets(C; X) all: x:A. B[x] top: Top presheaf-elements: el(P) mk-cat: mk-cat and: P ∧ Q
Lemmas referenced :  cat_ob_pair_lemma cat_ob_op_lemma top_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesisEquality sqequalHypSubstitution setElimination thin rename productElimination sqequalRule extract_by_obid dependent_functionElimination isect_memberEquality voidElimination voidEquality hypothesis equalityTransitivity equalitySymmetry sqequalAxiom isectElimination because_Cache

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[X:Top].    (cat-ob(sets(C;  X))  \msim{}  I:cat-ob(C)  \mtimes{}  X(I))



Date html generated: 2018_05_22-PM-09_59_09
Last ObjectModification: 2018_05_20-PM-09_41_59

Theory : presheaf!models!of!type!theory


Home Index