---

Step * 1 1 of Lemma yoneda-lemma


1. C : SmallCategory
2. x : cat-ob(C)
3. y : cat-ob(C)
4. a1 : cat-arrow(C) x y
5. a2 : cat-arrow(C) x y
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) (ob(rep-pre-sheaf(C;x)) A) (ob(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) (ob(rep-pre-sheaf(C;x)) A) (ob(rep-pre-sheaf(C;y)) A) (ob(rep-pre-sheaf(C;y)) B) 
       (A |→ λg.(cat-comp(C) A x y g a1) A) 
       (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) 
        (A |→ λg.(cat-comp(C) A x y g a1) B))
     ∈ (cat-arrow(TypeCat) (ob(rep-pre-sheaf(C;x)) A) (ob(rep-pre-sheaf(C;y)) B)))
⊢ a1 = a2 ∈ (cat-arrow(C) x y)
BY
{ (ApFunToHypEquands `Z' ⌜Z x (cat-id(C) x)⌝ ⌜cat-arrow(C) x y⌝ (-2)⋅ THEN RW CatNormC (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  x  :  cat-ob(C)
3.  y  :  cat-ob(C)
4.  a1  :  cat-arrow(C)  x  y
5.  a2  :  cat-arrow(C)  x  y
6.  A  |\mrightarrow{}  \mlambda{}g.(cat-comp(C)  A  x  y  g  a1)  =  A  |\mrightarrow{}  \mlambda{}g.(cat-comp(C)  A  x  y  g  a2)
7.  \mforall{}A,B:cat-ob(op-cat(C)).  \mforall{}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) 
              (A  |\mrightarrow{}  \mlambda{}g.(cat-comp(C)  A  x  y  g  a1)  A) 
              (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) 
                (A  |\mrightarrow{}  \mlambda{}g.(cat-comp(C)  A  x  y  g  a1)  B)))
\mvdash{}  a1  =  a2


By

---

Latex:
(ApFunToHypEquands  `Z'  \mkleeneopen{}Z  x  (cat-id(C)  x)\mkleeneclose{}  \mkleeneopen{}cat-arrow(C)  x  y\mkleeneclose{}  (-2)\mcdot{}  THEN  RW  CatNormC  (-1)  THEN  Auto)

---

Home Index