---

Step * 1 of Lemma monad-unit-extend


1. C : SmallCategory
2. T : Functor(C;C)
3. M2 : A:cat-ob(C) ⟶ (cat-arrow(C) A (T A))
4. ∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B.
     ((cat-comp(C) A (T A) (T B) (M2 A) (T A B g)) = (cat-comp(C) A B (T B) g (M2 B)) ∈ (cat-arrow(C) A (T B)))
5. M3 : A:cat-ob(C) ⟶ (cat-arrow(C) (T (T A)) (T A))
6. ∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B.
     ((cat-comp(C) (T (T A)) (T A) (T B) (M3 A) (T A B g))
     = (cat-comp(C) (T (T A)) (T (T B)) (T B) (T (T A) (T B) (T A B g)) (M3 B))
     ∈ (cat-arrow(C) (T (T A)) (T B)))
7. ∀X:cat-ob(C)
     ((cat-comp(C) (T X) (T (T X)) (T X) (M2 (T X)) (M3 X)) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X)))
8. ∀X:cat-ob(C)
     ((cat-comp(C) (T X) (T (T X)) (T X) (T X (T X) (M2 X)) (M3 X)) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X)))
9. ∀X:cat-ob(C)
     ((cat-comp(C) (T (T (T X))) (T (T X)) (T X) (M3 (T X)) (M3 X))
     = (cat-comp(C) (T (T (T X))) (T (T X)) (T X) (T (T (T X)) (T X) (M3 X)) (M3 X))
     ∈ (cat-arrow(C) (T (T (T X))) (T X)))
10. x : cat-ob(C)
11. y : cat-ob(C)
12. f : cat-arrow(C) x (T y)
⊢ (cat-comp(C) x (T x) (T y) (M2 x) (cat-comp(C) (T x) (T (T y)) (T y) (T x (T y) f) (M3 y)))
= f
∈ (cat-arrow(C) x (T y))
BY
{ ((RWO "cat-comp-assoc<" 0 THENA Auto) THEN RWO "4" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  T  :  Functor(C;C)
3.  M2  :  A:cat-ob(C)  {}\mrightarrow{}  (cat-arrow(C)  A  (T  A))
4.  \mforall{}A,B:cat-ob(C).  \mforall{}g:cat-arrow(C)  A  B.
          ((cat-comp(C)  A  (T  A)  (T  B)  (M2  A)  (T  A  B  g))  =  (cat-comp(C)  A  B  (T  B)  g  (M2  B)))
5.  M3  :  A:cat-ob(C)  {}\mrightarrow{}  (cat-arrow(C)  (T  (T  A))  (T  A))
6.  \mforall{}A,B:cat-ob(C).  \mforall{}g:cat-arrow(C)  A  B.
          ((cat-comp(C)  (T  (T  A))  (T  A)  (T  B)  (M3  A)  (T  A  B  g))
          =  (cat-comp(C)  (T  (T  A))  (T  (T  B))  (T  B)  (T  (T  A)  (T  B)  (T  A  B  g))  (M3  B)))
7.  \mforall{}X:cat-ob(C).  ((cat-comp(C)  (T  X)  (T  (T  X))  (T  X)  (M2  (T  X))  (M3  X))  =  (cat-id(C)  (T  X)))
8.  \mforall{}X:cat-ob(C).  ((cat-comp(C)  (T  X)  (T  (T  X))  (T  X)  (T  X  (T  X)  (M2  X))  (M3  X))  =  (cat-id(C)  (T  X)))
9.  \mforall{}X:cat-ob(C)
          ((cat-comp(C)  (T  (T  (T  X)))  (T  (T  X))  (T  X)  (M3  (T  X))  (M3  X))
          =  (cat-comp(C)  (T  (T  (T  X)))  (T  (T  X))  (T  X)  (T  (T  (T  X))  (T  X)  (M3  X))  (M3  X)))
10.  x  :  cat-ob(C)
11.  y  :  cat-ob(C)
12.  f  :  cat-arrow(C)  x  (T  y)
\mvdash{}  (cat-comp(C)  x  (T  x)  (T  y)  (M2  x)  (cat-comp(C)  (T  x)  (T  (T  y))  (T  y)  (T  x  (T  y)  f)  (M3  y)))  =  f


By

---

Latex:
((RWO  "cat-comp-assoc<"  0  THENA  Auto)  THEN  RWO  "4"  0  THEN  Auto)

---

Home Index