---

Step * 4 of Lemma yoneda-embedding_wf


1. C : SmallCategory
2. X : cat-ob(C)
⊢ A |→ λg.(cat-comp(C) A X X g (cat-id(C) X))
= identity-trans(op-cat(C);TypeCat;rep-pre-sheaf(C;X))
∈ nat-trans(op-cat(C);TypeCat;rep-pre-sheaf(C;X);rep-pre-sheaf(C;X))
BY
{ (RepUR ``functor-cat identity-trans`` 0 THEN EqCDA) }

1
.....subterm..... T:t
1:n
1. C : SmallCategory
2. X : cat-ob(C)
3. A : cat-ob(op-cat(C))
⊢ (λg.(cat-comp(C) A X X g (cat-id(C) X)))
= (cat-id(TypeCat) (ob(rep-pre-sheaf(C;X)) A))
∈ (cat-arrow(TypeCat) (ob(rep-pre-sheaf(C;X)) A) (ob(rep-pre-sheaf(C;X)) A))

2
.....antecedent..... 
1. C : SmallCategory
2. X : cat-ob(C)
⊢ ∀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;X)) A) (ob(rep-pre-sheaf(C;X)) B) 
      (λg.(cat-comp(C) A X X g (cat-id(C) X))) 
      (arrow(rep-pre-sheaf(C;X)) 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;X)) B) 
       (arrow(rep-pre-sheaf(C;X)) A B g) 
       (λg.(cat-comp(C) B X X g (cat-id(C) X))))
    ∈ (cat-arrow(TypeCat) (ob(rep-pre-sheaf(C;X)) A) (ob(rep-pre-sheaf(C;X)) B)))

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  X  :  cat-ob(C)
\mvdash{}  A  |\mrightarrow{}  \mlambda{}g.(cat-comp(C)  A  X  X  g  (cat-id(C)  X))  =  identity-trans(op-cat(C);TypeCat;rep-pre-sheaf(C;X))


By

---

Latex:
(RepUR  ``functor-cat  identity-trans``  0  THEN  EqCDA)

---

Home Index