---

Step * 1 1 of Lemma monad-extend-comp


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.  (T(g) o M2 A = M2 B o g ∈ (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.  (T(g) o M3 A = M3 B o T(T(g)) ∈ (cat-arrow(C) (T (T A)) (T B)))
7. ∀X:cat-ob(C). (M3 X o M2 (T X) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X)))
8. ∀X:cat-ob(C). (M3 X o T(M2 X) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X)))
9. ∀X:cat-ob(C). (M3 X o M3 (T X) = M3 X o T(M3 X) ∈ (cat-arrow(C) (T (T (T X))) (T X)))
10. x : cat-ob(C)
11. y : cat-ob(C)
12. z : cat-ob(C)
13. g : cat-arrow(C) x (T y)
14. h : cat-arrow(C) y (T z)
⊢ M3 z o T(M3 z) o T(T(h)) o T(g) = M3 z o T(h) o M3 y o T(g) ∈ (cat-arrow(C) (T x) (T z))
BY
{ ((RWW "cat_comp_assoc" 0 THENA Auto) THEN (RWO "9<" 0 THENA Auto)) }

1
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.  (T(g) o M2 A = M2 B o g ∈ (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.  (T(g) o M3 A = M3 B o T(T(g)) ∈ (cat-arrow(C) (T (T A)) (T B)))
7. ∀X:cat-ob(C). (M3 X o M2 (T X) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X)))
8. ∀X:cat-ob(C). (M3 X o T(M2 X) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X)))
9. ∀X:cat-ob(C). (M3 X o M3 (T X) = M3 X o T(M3 X) ∈ (cat-arrow(C) (T (T (T X))) (T X)))
10. x : cat-ob(C)
11. y : cat-ob(C)
12. z : cat-ob(C)
13. g : cat-arrow(C) x (T y)
14. h : cat-arrow(C) y (T z)
⊢ M3 z o M3 (T z) o T(T(h)) o T(g) = M3 z o T(h) o M3 y o T(g) ∈ (cat-arrow(C) (T x) (T z))

---

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.    (T(g)  o  M2  A  =  M2  B  o  g)
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.    (T(g)  o  M3  A  =  M3  B  o  T(T(g)))
7.  \mforall{}X:cat-ob(C).  (M3  X  o  M2  (T  X)  =  (cat-id(C)  (T  X)))
8.  \mforall{}X:cat-ob(C).  (M3  X  o  T(M2  X)  =  (cat-id(C)  (T  X)))
9.  \mforall{}X:cat-ob(C).  (M3  X  o  M3  (T  X)  =  M3  X  o  T(M3  X))
10.  x  :  cat-ob(C)
11.  y  :  cat-ob(C)
12.  z  :  cat-ob(C)
13.  g  :  cat-arrow(C)  x  (T  y)
14.  h  :  cat-arrow(C)  y  (T  z)
\mvdash{}  M3  z  o  T(M3  z)  o  T(T(h))  o  T(g)  =  M3  z  o  T(h)  o  M3  y  o  T(g)


By

---

Latex:
((RWW  "cat\_comp\_assoc"  0  THENA  Auto)  THEN  (RWO  "9<"  0  THENA  Auto))

---

Home Index