Nuprl Lemma : mk-presheaf_wf

[C:SmallCategory]. ∀[S:cat-ob(C) ⟶ Type]. ∀[morph:I:cat-ob(C) ⟶ J:cat-ob(C) ⟶ f:(cat-arrow(C) I) ⟶ S[I] ⟶ S[J]].
  (Presheaf(Set(I) =S[I];
            Morphism(I,J,f,rho) morph[I;J;f;rho]) ∈ Presheaf(C)) supposing 
     ((∀I,J,K:cat-ob(C). ∀f:cat-arrow(C) I. ∀g:cat-arrow(C) J. ∀rho:S[I].
         (morph[I;K;cat-comp(C) f;rho] morph[J;K;g;morph[I;J;f;rho]] ∈ S[K])) and 
     (∀I:cat-ob(C). ∀rho:S[I].  (morph[I;I;cat-id(C) I;rho] rho ∈ S[I])))


Definitions occuring in Statement :  mk-presheaf: mk-presheaf presheaf: Presheaf(C) cat-comp: cat-comp(C) cat-id: cat-id(C) cat-arrow: cat-arrow(C) cat-ob: cat-ob(C) small-category: SmallCategory uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s1;s2;s3;s4] so_apply: x[s] all: x:A. B[x] member: t ∈ T apply: a function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  member: t ∈ T uall: [x:A]. B[x] subtype_rel: A ⊆B so_apply: x[s] uimplies: supposing a all: x:A. B[x] top: Top type-cat: TypeCat so_apply: x[s1;s2;s3;s4] compose: g squash: T prop: true: True guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q mk-presheaf: mk-presheaf presheaf: Presheaf(C) so_lambda: λ2x.t[x] so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3]
Lemmas referenced :  op-cat_wf small-category-subtype type-cat_wf subtype_rel-equal cat-ob_wf cat_ob_op_lemma op-cat-arrow cat_arrow_triple_lemma cat-arrow_wf op-cat-comp cat_comp_tuple_lemma equal_wf squash_wf true_wf iff_weakening_equal op-cat-id cat_id_tuple_lemma mk-functor_wf all_wf cat-comp_wf cat-id_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut thin instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality applyEquality hypothesis sqequalRule functionExtensionality because_Cache independent_isectElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality lambdaEquality lambdaFormation imageElimination equalityTransitivity equalitySymmetry natural_numberEquality imageMemberEquality baseClosed universeEquality productElimination independent_functionElimination isect_memberFormation axiomEquality functionEquality cumulativity

\mforall{}[C:SmallCategory].  \mforall{}[S:cat-ob(C)  {}\mrightarrow{}  Type].  \mforall{}[morph:I:cat-ob(C)
                                                                                                        {}\mrightarrow{}  J:cat-ob(C)
                                                                                                        {}\mrightarrow{}  f:(cat-arrow(C)  J  I)
                                                                                                        {}\mrightarrow{}  S[I]
                                                                                                        {}\mrightarrow{}  S[J]].
    (Presheaf(Set(I)  =S[I];
                        Morphism(I,J,f,rho)  =  morph[I;J;f;rho])  \mmember{}  Presheaf(C))  supposing 
          ((\mforall{}I,J,K:cat-ob(C).  \mforall{}f:cat-arrow(C)  J  I.  \mforall{}g:cat-arrow(C)  K  J.  \mforall{}rho:S[I].
                  (morph[I;K;cat-comp(C)  K  J  I  g  f;rho]  =  morph[J;K;g;morph[I;J;f;rho]]))  and 
          (\mforall{}I:cat-ob(C).  \mforall{}rho:S[I].    (morph[I;I;cat-id(C)  I;rho]  =  rho)))

Date html generated: 2017_10_05-AM-00_47_06
Last ObjectModification: 2017_10_03-PM-01_57_52

Theory : small!categories

Home Index