---

Step * of Lemma ps-context-map-1

No Annotations
∀[C:SmallCategory]. ∀[I:cat-ob(C)].  (<cat-id(C) I> = 1(Yoneda(I)) ∈ Yoneda(I) ⟶ Yoneda(I))
BY
{ (Auto THEN BLemma `pscm-equal2` THEN Auto) }

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)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[I:cat-ob(C)].    (<cat-id(C)  I>  =  1(Yoneda(I)))


By

---

Latex:
(Auto  THEN  BLemma  `pscm-equal2`  THEN  Auto)

---

Home Index