---

Step * 2 1 of Lemma pscm-comp-context-map


1. C : SmallCategory
2. Gamma : ps_context{j:l}(C)
3. Delta : ps_context{j:l}(C)
4. sigma : psc_map{j:l}(C; Delta; Gamma)
5. I : cat-ob(C)
6. rho : Delta(I)
7. I1 : cat-ob(C)
8. x : Yoneda(I)(I1)
⊢ (sigma I1 x(rho)) = x((sigma)rho) ∈ Gamma(I1)
BY
{ (RepUR ``Yoneda I_set functor-ob`` -1 THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  Gamma  :  ps\_context\{j:l\}(C)
3.  Delta  :  ps\_context\{j:l\}(C)
4.  sigma  :  psc\_map\{j:l\}(C;  Delta;  Gamma)
5.  I  :  cat-ob(C)
6.  rho  :  Delta(I)
7.  I1  :  cat-ob(C)
8.  x  :  Yoneda(I)(I1)
\mvdash{}  (sigma  I1  x(rho))  =  x((sigma)rho)


By

---

Latex:
(RepUR  ``Yoneda  I\_set  functor-ob``  -1  THEN  Auto)

---

Home Index