---

Step * 2 1 1 1 1 of Lemma yoneda-lemma


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)
5. A : cat-ob(C)
6. x1 : ob(rep-pre-sheaf(C;x)) A
⊢ (b A x1) = (cat-comp(C) A x y x1 (b x (cat-id(C) x))) ∈ (ob(rep-pre-sheaf(C;y)) A)
BY
{ RepUR ``yoneda-embedding`` -3 }

1
1. C : SmallCategory
2. x : cat-ob(C)
3. y : cat-ob(C)
4. b : nat-trans(op-cat(C);TypeCat;rep-pre-sheaf(C;x);rep-pre-sheaf(C;y))
5. A : cat-ob(C)
6. x1 : ob(rep-pre-sheaf(C;x)) A
⊢ (b A x1) = (cat-comp(C) A x y x1 (b x (cat-id(C) x))) ∈ (ob(rep-pre-sheaf(C;y)) A)

---

Latex:

---

Latex:

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)
5.  A  :  cat-ob(C)
6.  x1  :  ob(rep-pre-sheaf(C;x))  A
\mvdash{}  (b  A  x1)  =  (cat-comp(C)  A  x  y  x1  (b  x  (cat-id(C)  x)))


By

---

Latex:
RepUR  ``yoneda-embedding``  -3

---

Home Index