---

Step * 1 of Lemma ext-equal-presheaves_wf


1. C : SmallCategory
2. F : Presheaf(C)
3. G : Presheaf(C)
4. ∀x:cat-ob(C). F x ≡ G x
5. x : cat-ob(C)@i
6. y : cat-ob(C)@i
7. f : cat-arrow(C) y x@i
⊢ G x y f ∈ (F x) ⟶ (F y)
BY
{ ((DoSubsume THEN Auto) THEN RepUR ``type-cat`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  F  :  Presheaf(C)
3.  G  :  Presheaf(C)
4.  \mforall{}x:cat-ob(C).  F  x  \mequiv{}  G  x
5.  x  :  cat-ob(C)@i
6.  y  :  cat-ob(C)@i
7.  f  :  cat-arrow(C)  y  x@i
\mvdash{}  G  x  y  f  \mmember{}  (F  x)  {}\mrightarrow{}  (F  y)


By

---

Latex:
((DoSubsume  THEN  Auto)  THEN  RepUR  ``type-cat``  0  THEN  Auto)

---

Home Index