---

Step * 2 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)
7. I@0 : cat-ob(C)
8. J : cat-ob(C)
9. f : cat-arrow(C) J I@0
10. a@0 : Yoneda(I)(I@0)
⊢ (ps-canonical-section(Gamma;A;I;rho;a) I@0 a@0 a@0 f)
= (ps-canonical-section(Gamma;A;I;rho;a) J f(a@0))
∈ A((<rho>)f(a@0))
BY
{ (RepUR ``Yoneda`` -1
   THEN RenameVar `K' (-4)
   THEN RenameVar `g' (-1)
   THEN RepUR ``ps-canonical-section`` 0
   THEN RepUR ``Yoneda`` 0) }

1
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)
7. K : cat-ob(C)
8. J : cat-ob(C)
9. f : cat-arrow(C) J K
10. g : cat-arrow(C) K I
⊢ ((a rho g) g f) = (a rho cat-comp(C) J K I f g) ∈ A((<rho>)cat-comp(C) J K I f g)

---

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)
7.  I@0  :  cat-ob(C)
8.  J  :  cat-ob(C)
9.  f  :  cat-arrow(C)  J  I@0
10.  a@0  :  Yoneda(I)(I@0)
\mvdash{}  (ps-canonical-section(Gamma;A;I;rho;a)  I@0  a@0  a@0  f)
=  (ps-canonical-section(Gamma;A;I;rho;a)  J  f(a@0))


By

---

Latex:
(RepUR  ``Yoneda``  -1
  THEN  RenameVar  `K'  (-4)
  THEN  RenameVar  `g'  (-1)
  THEN  RepUR  ``ps-canonical-section``  0
  THEN  RepUR  ``Yoneda``  0)

---

Home Index