---

Step * 1 of Lemma yoneda-lemma


1. C : SmallCategory@i'
2. x : cat-ob(C)@i
3. y : cat-ob(C)@i
4. a1 : cat-arrow(C) x y@i
5. a2 : cat-arrow(C) x y@i
6. (yoneda-embedding(C) x y a1)
= (yoneda-embedding(C) x y a2)
∈ (cat-arrow(FUN(op-cat(C);TypeCat)) (yoneda-embedding(C) x) (yoneda-embedding(C) y))
⊢ a1 = a2 ∈ (cat-arrow(C) x y)
BY
{ (RepUR ``yoneda-embedding`` -1 THEN (EqTypeHD (-1)⋅ THENA Auto)) }

1
1. C : SmallCategory@i'
2. x : cat-ob(C)@i
3. y : cat-ob(C)@i
4. a1 : cat-arrow(C) x y@i
5. a2 : cat-arrow(C) x y@i
6. A |→ λg.(cat-comp(C) A x y g a1)
= A |→ λg.(cat-comp(C) A x y g a2)
∈ (A:cat-ob(op-cat(C)) ⟶ (cat-arrow(TypeCat) (rep-pre-sheaf(C;x) A) (rep-pre-sheaf(C;y) A)))
7. ∀A,B:cat-ob(op-cat(C)). ∀g:cat-arrow(op-cat(C)) A B.
     ((cat-comp(TypeCat) (rep-pre-sheaf(C;x) A) (rep-pre-sheaf(C;y) A) (rep-pre-sheaf(C;y) B) 
       (A |→ λg.(cat-comp(C) A x y g a1) A) 
       (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) 
        (A |→ λg.(cat-comp(C) A x y g a1) B))
     ∈ (cat-arrow(TypeCat) (rep-pre-sheaf(C;x) A) (rep-pre-sheaf(C;y) B)))
⊢ a1 = a2 ∈ (cat-arrow(C) x y)

---

Latex:

---

Latex:

1.  C  :  SmallCategory@i'
2.  x  :  cat-ob(C)@i
3.  y  :  cat-ob(C)@i
4.  a1  :  cat-arrow(C)  x  y@i
5.  a2  :  cat-arrow(C)  x  y@i
6.  (yoneda-embedding(C)  x  y  a1)  =  (yoneda-embedding(C)  x  y  a2)
\mvdash{}  a1  =  a2


By

---

Latex:
(RepUR  ``yoneda-embedding``  -1  THEN  (EqTypeHD  (-1)\mcdot{}  THENA  Auto))

---

Home Index