---

Step * of Lemma yoneda-embedding_wf

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

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

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

3
1. C : SmallCategory
2. X : cat-ob(C)@i
3. Y : cat-ob(C)@i
4. z : cat-ob(C)@i
5. f : cat-arrow(C) X Y@i
6. g : cat-arrow(C) Y z@i
⊢ 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)@i
⊢ 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:
No  Annotations
\mforall{}[C:SmallCategory].  (yoneda-embedding(C)  \mmember{}  Functor(C;FUN(op-cat(C);TypeCat)))


By

---

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

---

Home Index