---

Step * 2 1 of Lemma yoneda-lemma


1. C : SmallCategory
2. x : cat-ob(C)
3. y : cat-ob(C)
4. b : cat-arrow(FUN(op-cat(C);TypeCat)) (ob(yoneda-embedding(C)) x) (ob(yoneda-embedding(C)) y)
⊢ (arrow(yoneda-embedding(C)) x y (b x (cat-id(C) x)))
= b
∈ (cat-arrow(FUN(op-cat(C);TypeCat)) (ob(yoneda-embedding(C)) x) (ob(yoneda-embedding(C)) y))
BY
{ (Symmetry THEN All (RepUR ``functor-cat``) THEN (BLemma `nat-trans-equal` THENW Auto)) }

1
1. C : SmallCategory
2. x : cat-ob(C)
3. y : cat-ob(C)
4. b : nat-trans(op-cat(C);TypeCat;ob(yoneda-embedding(C)) x;ob(yoneda-embedding(C)) y)
⊢ b
= (arrow(yoneda-embedding(C)) x y (b x (cat-id(C) x)))
∈ (A:cat-ob(op-cat(C)) ⟶ (cat-arrow(TypeCat) (ob(ob(yoneda-embedding(C)) x) A) (ob(ob(yoneda-embedding(C)) y) A)))

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  x  :  cat-ob(C)
3.  y  :  cat-ob(C)
4.  b  :  cat-arrow(FUN(op-cat(C);TypeCat))  (ob(yoneda-embedding(C))  x)  (ob(yoneda-embedding(C))  y)
\mvdash{}  (arrow(yoneda-embedding(C))  x  y  (b  x  (cat-id(C)  x)))  =  b


By

---

Latex:
(Symmetry  THEN  All  (RepUR  ``functor-cat``)  THEN  (BLemma  `nat-trans-equal`  THENW  Auto))

---

Home Index