---

Step * 1 of Lemma ps-context-map-1


1. C : SmallCategory
2. I : cat-ob(C)
3. K : cat-ob(C)
4. x : Yoneda(I)(K)
⊢ (<cat-id(C) I> K x) = (1(Yoneda(I)) K x) ∈ Yoneda(I)(K)
BY
{ (RepUR ``ps-context-map pscm-id Yoneda functor-arrow`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  I  :  cat-ob(C)
3.  K  :  cat-ob(C)
4.  x  :  Yoneda(I)(K)
\mvdash{}  (<cat-id(C)  I>  K  x)  =  (1(Yoneda(I))  K  x)


By

---

Latex:
(RepUR  ``ps-context-map  pscm-id  Yoneda  functor-arrow``  0  THEN  Auto)

---

Home Index