---

Step * of Lemma equal-presheaves

No Annotations
∀[C:SmallCategory]. ∀[F,G:Presheaf(C)].
  F = G ∈ Presheaf(C) 
  supposing (∀x:cat-ob(op-cat(C)). ((F x) = (G x) ∈ cat-ob(TypeCat)))
  ∧ (∀x,y:cat-ob(op-cat(C)). ∀f:cat-arrow(op-cat(C)) x y.  ((F x y f) = (G x y f) ∈ (cat-arrow(TypeCat) (F x) (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:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[F,G:Presheaf(C)].
    F  =  G 
    supposing  (\mforall{}x:cat-ob(op-cat(C)).  ((F  x)  =  (G  x)))
    \mwedge{}  (\mforall{}x,y:cat-ob(op-cat(C)).  \mforall{}f:cat-arrow(op-cat(C))  x  y.    ((F  x  y  f)  =  (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