Nuprl Lemma : mk-presheaf_wf1

[C:SmallCategory]. ∀[S:cat-ob(C) ⟶ 𝕌{j}]. ∀[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{j:l}(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] cat-ob: cat-ob(C) pi1: fst(t) type-cat: TypeCat so_apply: x[s1;s2;s3;s4] compose: g guard: {T} mk-presheaf: mk-presheaf presheaf: Presheaf(C) so_lambda: λ2x.t[x] so_lambda: so_lambda3 so_apply: x[s1;s2;s3]
Lemmas referenced :  op-cat_wf small-category-cumulativity-2 type-cat_wf subtype_rel-equal cat-ob_wf cat_ob_op_lemma subtype_rel_self op-cat-arrow cat_arrow_triple_lemma cat-arrow_wf op-cat-comp cat_comp_tuple_lemma op-cat-id cat_id_tuple_lemma mk-functor_wf cat-comp_wf cat-id_wf istype-universe small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut thin instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality applyEquality hypothesis sqequalRule because_Cache independent_isectElimination dependent_functionElimination universeIsType Error :memTop,  lambdaEquality_alt lambdaFormation_alt functionExtensionality_alt isect_memberFormation_alt axiomEquality equalityTransitivity equalitySymmetry functionIsType equalityIstype isect_memberEquality_alt isectIsTypeImplies inhabitedIsType universeEquality

\mforall{}[C:SmallCategory].  \mforall{}[S:cat-ob(C)  {}\mrightarrow{}  \mBbbU{}\{j\}].  \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\{j:l\}(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: 2020_05_20-AM-07_52_54
Last ObjectModification: 2020_04_03-AM-11_26_55

Theory : small!categories

Home Index