---

Step * of Lemma mk-presheaf_wf

∀[C:SmallCategory]. ∀[S:cat-ob(C) ⟶ Type]. ∀[morph:I:cat-ob(C) ⟶ J:cat-ob(C) ⟶ f:(cat-arrow(C) J 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) J I. ∀g:cat-arrow(C) K J. ∀rho:S[I].
         (morph[I;K;cat-comp(C) K J I g 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])))
BY
{ ((Auto THEN Unfolds ``mk-presheaf presheaf`` 0 THEN MemCD)
   THEN Try (QuickAuto)
   THEN (All (RWO "cat_ob_op_lemma op-cat-arrow op-cat-comp op-cat-id") THENA Auto)
   THEN RepUR ``type-cat`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\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)))


By

---

Latex:
((Auto  THEN  Unfolds  ``mk-presheaf  presheaf``  0  THEN  MemCD)
  THEN  Try  (QuickAuto)
  THEN  (All  (RWO  "cat\_ob\_op\_lemma  op-cat-arrow  op-cat-comp  op-cat-id")  THENA  Auto)
  THEN  RepUR  ``type-cat``  0
  THEN  Auto)

---

Home Index