---

Step * of Lemma representable-psc_wf

∀[C:small-category{1:l}]. (representable-psc(C) ∈ 𝕌{3})
BY
{ (Auto THEN Unfold `representable-psc` 0) }

1
1. C : small-category{1:l}
⊢ {G:ps_context{1:l}(C)| ∃I:cat-ob(C). (G = Yoneda(I) ∈ ps_context{1:l}(C))}  ∈ 𝕌{3}

---

Latex:

---

Latex:
\mforall{}[C:small-category\{1:l\}].  (representable-psc(C)  \mmember{}  \mBbbU{}\{3\})


By

---

Latex:
(Auto  THEN  Unfold  `representable-psc`  0)

---

Home Index