---

Step * of Lemma unit-set-presheaf-type

∀[C:SmallCategory]. ∀[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
{ Auto }

1
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))))} 

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[I:cat-ob(C)].
    (\{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:
Auto

---

Home Index