---

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


1. C : SmallCategory@i'
2. x : cat-ob(C)@i
3. y : cat-ob(C)@i
4. b : nat-trans(op-cat(C);TypeCat;rep-pre-sheaf(C;x);rep-pre-sheaf(C;y))@i'
5. A : cat-ob(C)
6. x1 : rep-pre-sheaf(C;x) A
⊢ (b A x1) = (cat-comp(C) A x y x1 (b x (cat-id(C) x))) ∈ (rep-pre-sheaf(C;y) A)
BY
{ DVar `b' }

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

---

Latex:

---

Latex:

1.  C  :  SmallCategory@i'
2.  x  :  cat-ob(C)@i
3.  y  :  cat-ob(C)@i
4.  b  :  nat-trans(op-cat(C);TypeCat;rep-pre-sheaf(C;x);rep-pre-sheaf(C;y))@i'
5.  A  :  cat-ob(C)
6.  x1  :  rep-pre-sheaf(C;x)  A
\mvdash{}  (b  A  x1)  =  (cat-comp(C)  A  x  y  x1  (b  x  (cat-id(C)  x)))


By

---

Latex:
DVar  `b'

---

Home Index