---

Step * 2 1 1 1 of Lemma yoneda-lemma


1. C : SmallCategory@i'
2. x : cat-ob(C)@i
3. y : cat-ob(C)@i
4. b : nat-trans(op-cat(C);TypeCat;yoneda-embedding(C) x;yoneda-embedding(C) y)@i'
5. A : cat-ob(C)
⊢ (b A)
= (yoneda-embedding(C) x y (b x (cat-id(C) x)) A)
∈ (cat-arrow(TypeCat) (yoneda-embedding(C) x A) (yoneda-embedding(C) y A))
BY
{ (RepUR  ``yoneda-embedding type-cat`` 0
   THEN Try (Fold `mk-functor` 0)
   THEN Reduce 0
   THEN (FunExt THENA Auto)
   THEN Reduce 0) }

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

---

Latex:

---

Latex:

1.  C  :  SmallCategory@i'
2.  x  :  cat-ob(C)@i
3.  y  :  cat-ob(C)@i
4.  b  :  nat-trans(op-cat(C);TypeCat;yoneda-embedding(C)  x;yoneda-embedding(C)  y)@i'
5.  A  :  cat-ob(C)
\mvdash{}  (b  A)  =  (yoneda-embedding(C)  x  y  (b  x  (cat-id(C)  x))  A)


By

---

Latex:
(RepUR    ``yoneda-embedding  type-cat``  0
  THEN  Try  (Fold  `mk-functor`  0)
  THEN  Reduce  0
  THEN  (FunExt  THENA  Auto)
  THEN  Reduce  0)

---

Home Index