---

Step * 1 of Lemma ps-canonical-section_wf


1. C : SmallCategory
2. Gamma : ps_context{j:l}(C)
3. A : {Gamma ⊢ _}
4. I : cat-ob(C)
5. rho : Gamma(I)
6. a : A(rho)
⊢ ps-canonical-section(Gamma;A;I;rho;a) ∈ I@0:cat-ob(C) ⟶ a:Yoneda(I)(I@0) ⟶ (A)<rho>(a)
BY
{ (RepUR ``Yoneda`` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  Gamma  :  ps\_context\{j:l\}(C)
3.  A  :  \{Gamma  \mvdash{}  \_\}
4.  I  :  cat-ob(C)
5.  rho  :  Gamma(I)
6.  a  :  A(rho)
\mvdash{}  ps-canonical-section(Gamma;A;I;rho;a)  \mmember{}  I@0:cat-ob(C)  {}\mrightarrow{}  a:Yoneda(I)(I@0)  {}\mrightarrow{}  (A)<rho>(a)


By

---

Latex:
(RepUR  ``Yoneda``  0  THEN  ProveWfLemma)

---

Home Index