---

Step * of Lemma equal-presheaves

∀[C:SmallCategory]. ∀[F,G:Presheaf(C)].
  F = G ∈ Presheaf(C) 
  supposing (∀x:cat-ob(op-cat(C)). ((ob(F) x) = (ob(G) x) ∈ cat-ob(TypeCat)))
  ∧ (∀x,y:cat-ob(op-cat(C)). ∀f:cat-arrow(op-cat(C)) x y.
       ((arrow(F) x y f) = (arrow(G) x y f) ∈ (cat-arrow(TypeCat) (ob(F) x) (ob(F) y))))
BY
{ (Auto
   THEN All
   (Unfold `presheaf`)⋅
   THEN InstLemma `equal-functors` [⌜parm{i'}⌝;⌜op-cat(C)⌝;⌜TypeCat⌝;⌜F⌝;⌜G⌝]⋅
   THEN Try (Complete (Auto))) }

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[F,G:Presheaf(C)].
    F  =  G 
    supposing  (\mforall{}x:cat-ob(op-cat(C)).  ((ob(F)  x)  =  (ob(G)  x)))
    \mwedge{}  (\mforall{}x,y:cat-ob(op-cat(C)).  \mforall{}f:cat-arrow(op-cat(C))  x  y.    ((arrow(F)  x  y  f)  =  (arrow(G)  x  y  f)))


By

---

Latex:
(Auto
  THEN  All
  (Unfold  `presheaf`)\mcdot{}
  THEN  InstLemma  `equal-functors`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}op-cat(C)\mkleeneclose{};\mkleeneopen{}TypeCat\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{}]\mcdot{}
  THEN  Try  (Complete  (Auto)))

---

Home Index