---

Step * 2 of Lemma yoneda-lemma


1. C : SmallCategory@i'
2. x : cat-ob(C)@i
3. y : cat-ob(C)@i
4. b : cat-arrow(FUN(op-cat(C);TypeCat)) (yoneda-embedding(C) x) (yoneda-embedding(C) y)@i'
⊢ ∃a:cat-arrow(C) x y
   ((yoneda-embedding(C) x y a)
   = b
   ∈ (cat-arrow(FUN(op-cat(C);TypeCat)) (yoneda-embedding(C) x) (yoneda-embedding(C) y)))
BY
{ (With ⌜b x (cat-id(C) x)⌝ (D 0)⋅ THENW Auto) }

1
1. C : SmallCategory@i'
2. x : cat-ob(C)@i
3. y : cat-ob(C)@i
4. b : cat-arrow(FUN(op-cat(C);TypeCat)) (yoneda-embedding(C) x) (yoneda-embedding(C) y)@i'
⊢ (yoneda-embedding(C) x y (b x (cat-id(C) x)))
= b
∈ (cat-arrow(FUN(op-cat(C);TypeCat)) (yoneda-embedding(C) x) (yoneda-embedding(C) y))

---

Latex:

---

Latex:

1.  C  :  SmallCategory@i'
2.  x  :  cat-ob(C)@i
3.  y  :  cat-ob(C)@i
4.  b  :  cat-arrow(FUN(op-cat(C);TypeCat))  (yoneda-embedding(C)  x)  (yoneda-embedding(C)  y)@i'
\mvdash{}  \mexists{}a:cat-arrow(C)  x  y.  ((yoneda-embedding(C)  x  y  a)  =  b)


By

---

Latex:
(With  \mkleeneopen{}b  x  (cat-id(C)  x)\mkleeneclose{}  (D  0)\mcdot{}  THENW  Auto)

---

Home Index