Nuprl Lemma : rep-pre-sheaf_wf

[C:SmallCategory]. ∀[X:cat-ob(C)].  (rep-pre-sheaf(C;X) ∈ Functor(op-cat(C);TypeCat))


Proof




Definitions occuring in Statement :  rep-pre-sheaf: rep-pre-sheaf(C;X) type-cat: TypeCat op-cat: op-cat(C) cat-functor: Functor(C1;C2) cat-ob: cat-ob(C) small-category: SmallCategory uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  prop: so_apply: x[s] so_lambda: λ2x.t[x] all: x:A. B[x] cand: c∧ B and: P ∧ Q compose: g cat-id: cat-id(C) subtype_rel: A ⊆B pi2: snd(t) pi1: fst(t) spreadn: spread4 cat-ob: cat-ob(C) op-cat: op-cat(C) type-cat: TypeCat cat-arrow: cat-arrow(C) cat-comp: cat-comp(C) small-category: SmallCategory cat-functor: Functor(C1;C2) rep-pre-sheaf: rep-pre-sheaf(C;X) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  small-category_wf cat-comp_wf cat-id_wf type-cat_wf cat-arrow_wf equal_wf op-cat_wf cat-ob_wf all_wf subtype_rel_self
Rules used in proof :  isect_memberEquality equalitySymmetry equalityTransitivity axiomEquality universeEquality instantiate productEquality independent_pairFormation dependent_functionElimination functionExtensionality lambdaFormation functionEquality because_Cache cumulativity hypothesis isectElimination lemma_by_obid hypothesisEquality applyEquality lambdaEquality dependent_pairEquality sqequalRule productElimination rename thin setElimination sqequalHypSubstitution dependent_set_memberEquality cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[X:cat-ob(C)].    (rep-pre-sheaf(C;X)  \mmember{}  Functor(op-cat(C);TypeCat))



Date html generated: 2016_05_18-AM-11_53_27
Last ObjectModification: 2015_12_28-PM-02_23_30

Theory : small!categories


Home Index