---

Step * 2 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)
⊢ (sigma o <rho> I1) = (<(sigma)rho> I1) ∈ (Yoneda(I)(I1) ⟶ Gamma(I1))
BY
{ (RepUR ``pscm-comp ps-context-map functor-arrow compose`` 0
   THEN Fold `psc-restriction` 0
   THEN (FunExt THENA Auto)
   THEN Reduce 0) }

1
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)

---

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)
\mvdash{}  (sigma  o  <rho>  I1)  =  (<(sigma)rho>  I1)


By

---

Latex:
(RepUR  ``pscm-comp  ps-context-map  functor-arrow  compose``  0
  THEN  Fold  `psc-restriction`  0
  THEN  (FunExt  THENA  Auto)
  THEN  Reduce  0)

---

Home Index