---

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


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))))
BY
{ Repeat ((EqCD THEN Try ((Trivial ORELSE Complete (Computation))))) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  I  :  cat-ob(C)
3.  AF  :  Base
4.  A  :  Base
5.  F  :  Base
\mvdash{}  (\mforall{}I@0:cat-ob(C).  \mforall{}a:Yoneda(I)(I@0).  \mforall{}u:A  I@0  a.    ((F  I@0  I@0  (cat-id(C)  I@0)  a  u)  =  u))
\mwedge{}  (\mforall{}I@0,J,K:cat-ob(C).  \mforall{}f:cat-arrow(C)  J  I@0.  \mforall{}g:cat-arrow(C)  K  J.  \mforall{}a:Yoneda(I)(I@0).  \mforall{}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)))) 
\msim{}  (\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:
Repeat  ((EqCD  THEN  Try  ((Trivial  ORELSE  Complete  (Computation)))))

---

Home Index