---

Step * of Lemma yoneda-embedding_wf

∀[C:SmallCategory]. (yoneda-embedding(C) ∈ Functor(C;FUN(op-cat(C);TypeCat)))
BY
{ (Intros THEN Unfold `yoneda-embedding` 0 THEN MemCD THEN Reduce 0 THEN Auto) }

1
1. C : SmallCategory
2. X : cat-ob(C)
3. Y : cat-ob(C)
4. f : cat-arrow(C) X Y
5. A : cat-ob(op-cat(C))
⊢ λg.(cat-comp(C) A X Y g f) ∈ cat-arrow(TypeCat) (ob(rep-pre-sheaf(C;X)) A) (ob(rep-pre-sheaf(C;Y)) A)

2
1. C : SmallCategory
2. X : cat-ob(C)
3. Y : cat-ob(C)
4. f : cat-arrow(C) X Y
5. A : cat-ob(op-cat(C))
6. B : cat-ob(op-cat(C))
7. g : cat-arrow(op-cat(C)) A B
⊢ (cat-comp(TypeCat) (ob(rep-pre-sheaf(C;X)) A) (ob(rep-pre-sheaf(C;Y)) A) (ob(rep-pre-sheaf(C;Y)) B) 
   (λg.(cat-comp(C) A X Y g f)) 
   (arrow(rep-pre-sheaf(C;Y)) A B g))
= (cat-comp(TypeCat) (ob(rep-pre-sheaf(C;X)) A) (ob(rep-pre-sheaf(C;X)) B) (ob(rep-pre-sheaf(C;Y)) B) 
   (arrow(rep-pre-sheaf(C;X)) A B g) 
   (λg.(cat-comp(C) B X Y g f)))
∈ (cat-arrow(TypeCat) (ob(rep-pre-sheaf(C;X)) A) (ob(rep-pre-sheaf(C;Y)) B))

3
1. C : SmallCategory
2. X : cat-ob(C)
3. Y : cat-ob(C)
4. z : cat-ob(C)
5. f : cat-arrow(C) X Y
6. g : cat-arrow(C) Y z
⊢ A |→ λg@0.(cat-comp(C) A X z g@0 (cat-comp(C) X Y z f g))
= A |→ λg.(cat-comp(C) A X Y g f) o A |→ λg@0.(cat-comp(C) A Y z g@0 g)
∈ nat-trans(op-cat(C);TypeCat;rep-pre-sheaf(C;X);rep-pre-sheaf(C;z))

4
1. C : SmallCategory
2. X : cat-ob(C)
⊢ A |→ λg.(cat-comp(C) A X X g (cat-id(C) X))
= identity-trans(op-cat(C);TypeCat;rep-pre-sheaf(C;X))
∈ nat-trans(op-cat(C);TypeCat;rep-pre-sheaf(C;X);rep-pre-sheaf(C;X))

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  (yoneda-embedding(C)  \mmember{}  Functor(C;FUN(op-cat(C);TypeCat)))


By

---

Latex:
(Intros  THEN  Unfold  `yoneda-embedding`  0  THEN  MemCD  THEN  Reduce  0  THEN  Auto)

---

Home Index