---

Step * 4 of Lemma yoneda-embedding_wf


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

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

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  X  :  cat-ob(C)@i
\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