---

Step * of Lemma Yoneda_wf

No Annotations
∀[C:SmallCategory]. ∀[I:cat-ob(C)].  (Yoneda(I) ∈ __⊢)
BY
{ (Unfold `ps_context` 0 THEN RWO "Yoneda-is-rep-pre-sheaf" 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[I:cat-ob(C)].    (Yoneda(I)  \mmember{}  \_\_\mvdash{})


By

---

Latex:
(Unfold  `ps\_context`  0  THEN  RWO  "Yoneda-is-rep-pre-sheaf"  0  THEN  Auto)

---

Home Index