---

Step * 2 1 1 1 1 1 1 1 1 1 2 of Lemma yoneda-lemma


1. C : SmallCategory
2. x : cat-ob(C)
3. y : cat-ob(C)
4. b : A:cat-ob(op-cat(C)) ⟶ (cat-arrow(TypeCat) (ob(rep-pre-sheaf(C;x)) A) (ob(rep-pre-sheaf(C;y)) A))
5. ∀A,B:cat-ob(C). ∀g:cat-arrow(C) B A.
     (((arrow(rep-pre-sheaf(C;y)) A B g) o (b A))
     = ((b B) o (arrow(rep-pre-sheaf(C;x)) A B g))
     ∈ ((ob(rep-pre-sheaf(C;x)) A) ⟶ (ob(rep-pre-sheaf(C;y)) B)))
6. A : cat-ob(C)
7. x1 : cat-arrow(C) A x
8. ((λux.(cat-comp(C) A x y x1 ux)) o (b x))
= ((b A) o (λux.(cat-comp(C) A x x x1 ux)))
∈ ((cat-arrow(C) x x) ⟶ (cat-arrow(C) A y))
9. (((λux.(cat-comp(C) A x y x1 ux)) o (b x)) (cat-id(C) x))
= (((b A) o (λux.(cat-comp(C) A x x x1 ux))) (cat-id(C) x))
∈ (cat-arrow(C) A y)
⊢ (b A x1) = (cat-comp(C) A x y x1 (b x (cat-id(C) x))) ∈ (cat-arrow(C) A y)
BY
{ (RW CatNormC (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  x  :  cat-ob(C)
3.  y  :  cat-ob(C)
4.  b  :  A:cat-ob(op-cat(C))  {}\mrightarrow{}  (cat-arrow(TypeCat)  (ob(rep-pre-sheaf(C;x))  A) 
                                                              (ob(rep-pre-sheaf(C;y))  A))
5.  \mforall{}A,B:cat-ob(C).  \mforall{}g:cat-arrow(C)  B  A.
          (((arrow(rep-pre-sheaf(C;y))  A  B  g)  o  (b  A))  =  ((b  B)  o  (arrow(rep-pre-sheaf(C;x))  A  B  g)))
6.  A  :  cat-ob(C)
7.  x1  :  cat-arrow(C)  A  x
8.  ((\mlambda{}ux.(cat-comp(C)  A  x  y  x1  ux))  o  (b  x))  =  ((b  A)  o  (\mlambda{}ux.(cat-comp(C)  A  x  x  x1  ux)))
9.  (((\mlambda{}ux.(cat-comp(C)  A  x  y  x1  ux))  o  (b  x))  (cat-id(C)  x))
=  (((b  A)  o  (\mlambda{}ux.(cat-comp(C)  A  x  x  x1  ux)))  (cat-id(C)  x))
\mvdash{}  (b  A  x1)  =  (cat-comp(C)  A  x  y  x1  (b  x  (cat-id(C)  x)))


By

---

Latex:
(RW  CatNormC  (-1)  THEN  Auto)

---

Home Index