---

Step * 1 of Lemma unit-set-presheaf-type


1. C : SmallCategory
2. I : cat-ob(C)
⊢ {Yoneda(I) ⊢ _} ~ {AF:A:L:cat-ob(C) ⟶ (cat-arrow(C) L I) ⟶ Type × (L:cat-ob(C)
                                                                      ⟶ J:cat-ob(C)
                                                                      ⟶ f:(cat-arrow(C) J L)
                                                                      ⟶ a:(cat-arrow(C) L I)
                                                                      ⟶ (A L a)
                                                                      ⟶ (A J (cat-comp(C) J L I f a)))| 
                     let A,F = AF 
                     in (∀K:cat-ob(C). ∀a:cat-arrow(C) K I. ∀u:A K a.  ((F K K (cat-id(C) K) a u) = u ∈ (A K a)))
                        ∧ (∀L,J,K:cat-ob(C). ∀f:cat-arrow(C) J L. ∀g:cat-arrow(C) K J. ∀a:cat-arrow(C) L I. ∀u:A L a.
                             ((F L K (cat-comp(C) K J L g f) a u)
                             = (F J K g (cat-comp(C) J L I f a) (F L J f a u))
                             ∈ (A K (cat-comp(C) K L I (cat-comp(C) K J L g f) a))))} 
BY
{ (Computation THEN EqCD THEN Try (Trivial)) }

1
1. C : SmallCategory
2. I : cat-ob(C)
3. A : Base
4. I@0 : Base
5. J : Base
6. f : Base
7. a : Base
8. @0 : Base
⊢ f(a) ~ cat-comp(C) J I@0 I f a

2
1. C : SmallCategory
2. I : cat-ob(C)
3. AF : Base
4. A : Base
5. F : Base
⊢ (∀I@0:cat-ob(C). ∀a:Yoneda(I)(I@0). ∀u:A I@0 a.  ((F I@0 I@0 (cat-id(C) I@0) a u) = u ∈ (A I@0 a)))
∧ (∀I@0,J,K:cat-ob(C). ∀f:cat-arrow(C) J I@0. ∀g:cat-arrow(C) K J. ∀a:Yoneda(I)(I@0). ∀u:A I@0 a.
     ((F I@0 K (cat-comp(C) K J I@0 g f) a u) = (F J K g f(a) (F I@0 J f a u)) ∈ (A K cat-comp(C) K J I@0 g f(a)))) 
~ (∀K:cat-ob(C). ∀a:cat-arrow(C) K I. ∀u:A K a.  ((F K K (cat-id(C) K) a u) = u ∈ (A K a)))
∧ (∀L,J,K:cat-ob(C). ∀f:cat-arrow(C) J L. ∀g:cat-arrow(C) K J. ∀a:cat-arrow(C) L I. ∀u:A L a.
     ((F L K (cat-comp(C) K J L g f) a u)
     = (F J K g (cat-comp(C) J L I f a) (F L J f a u))
     ∈ (A K (cat-comp(C) K L I (cat-comp(C) K J L g f) a))))

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  I  :  cat-ob(C)
\mvdash{}  \{Yoneda(I)  \mvdash{}  \_\}  \msim{}  \{AF:A:L:cat-ob(C)  {}\mrightarrow{}  (cat-arrow(C)  L  I)  {}\mrightarrow{}  Type  \mtimes{}  (L:cat-ob(C)
                                                                                                                                            {}\mrightarrow{}  J:cat-ob(C)
                                                                                                                                            {}\mrightarrow{}  f:(cat-arrow(C)  J  L)
                                                                                                                                            {}\mrightarrow{}  a:(cat-arrow(C)  L  I)
                                                                                                                                            {}\mrightarrow{}  (A  L  a)
                                                                                                                                            {}\mrightarrow{}  (A  J 
                                                                                                                                                    (cat-comp(C)  J  L  I  f 
                                                                                                                                                      a)))| 
                                          let  A,F  =  AF 
                                          in  (\mforall{}K:cat-ob(C).  \mforall{}a:cat-arrow(C)  K  I.  \mforall{}u:A  K  a.
                                                      ((F  K  K  (cat-id(C)  K)  a  u)  =  u))
                                                \mwedge{}  (\mforall{}L,J,K:cat-ob(C).  \mforall{}f:cat-arrow(C)  J  L.  \mforall{}g:cat-arrow(C)  K  J.
                                                      \mforall{}a:cat-arrow(C)  L  I.  \mforall{}u:A  L  a.
                                                          ((F  L  K  (cat-comp(C)  K  J  L  g  f)  a  u)
                                                          =  (F  J  K  g  (cat-comp(C)  J  L  I  f  a)  (F  L  J  f  a  u))))\} 


By

---

Latex:
(Computation  THEN  EqCD  THEN  Try  (Trivial))

---

Home Index