---

Step * of Lemma ext-equal-presheaves_wf

No Annotations
∀[C:SmallCategory]. ∀[F,G:Presheaf(C)].  (ext-equal-presheaves(C;F;G) ∈ ℙ')
BY
{ ProveWfLemma }

1
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)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[F,G:Presheaf(C)].    (ext-equal-presheaves(C;F;G)  \mmember{}  \mBbbP{}')


By

---

Latex:
ProveWfLemma

---

Home Index