---

Step * of Lemma monad-extend-comp

∀[C:SmallCategory]. ∀[M:Monad(C)]. ∀[x,y,z:cat-ob(C)]. ∀[g:cat-arrow(C) x M(y)]. ∀[h:cat-arrow(C) y M(z)].
  (monad-extend(C;M;x;z;cat-comp(C) x M(y) M(z) g monad-extend(C;M;y;z;h))
  = (cat-comp(C) M(x) M(y) M(z) monad-extend(C;M;x;y;g) monad-extend(C;M;y;z;h))
  ∈ (cat-arrow(C) M(x) M(z)))
BY
{ (Auto
   THEN DVar `M'
   THEN DProds
   THEN DVar `M2'
   THEN DVar `M3'
   THEN (All (RepUR ``id_functor functor-comp monad-extend monad-fun``)
         THEN All (RepUR ``monad-functor monad-unit monad-op``)
         )
   THEN All Reduce
   THEN ExRepD) }

1
1. C : SmallCategory
2. T : Functor(C;C)
3. M2 : A:cat-ob(C) ⟶ (cat-arrow(C) A (ob(T) A))
4. ∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B.
     ((cat-comp(C) A (ob(T) A) (ob(T) B) (M2 A) (arrow(T) A B g))
     = (cat-comp(C) A B (ob(T) B) g (M2 B))
     ∈ (cat-arrow(C) A (ob(T) B)))
5. M3 : A:cat-ob(C) ⟶ (cat-arrow(C) (ob(T) (ob(T) A)) (ob(T) A))
6. ∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B.
     ((cat-comp(C) (ob(T) (ob(T) A)) (ob(T) A) (ob(T) B) (M3 A) (arrow(T) A B g))
     = (cat-comp(C) (ob(T) (ob(T) A)) (ob(T) (ob(T) B)) (ob(T) B) (arrow(T) (ob(T) A) (ob(T) B) (arrow(T) A B g)) 
        (M3 B))
     ∈ (cat-arrow(C) (ob(T) (ob(T) A)) (ob(T) B)))
7. ∀X:cat-ob(C)
     ((cat-comp(C) (ob(T) X) (ob(T) (ob(T) X)) (ob(T) X) (M2 (ob(T) X)) (M3 X))
     = (cat-id(C) (ob(T) X))
     ∈ (cat-arrow(C) (ob(T) X) (ob(T) X)))
8. ∀X:cat-ob(C)
     ((cat-comp(C) (ob(T) X) (ob(T) (ob(T) X)) (ob(T) X) (arrow(T) X (ob(T) X) (M2 X)) (M3 X))
     = (cat-id(C) (ob(T) X))
     ∈ (cat-arrow(C) (ob(T) X) (ob(T) X)))
9. ∀X:cat-ob(C)
     ((cat-comp(C) (ob(T) (ob(T) (ob(T) X))) (ob(T) (ob(T) X)) (ob(T) X) (M3 (ob(T) X)) (M3 X))
     = (cat-comp(C) (ob(T) (ob(T) (ob(T) X))) (ob(T) (ob(T) X)) (ob(T) X) (arrow(T) (ob(T) (ob(T) X)) (ob(T) X) (M3 X)) 
        (M3 X))
     ∈ (cat-arrow(C) (ob(T) (ob(T) (ob(T) X))) (ob(T) X)))
10. x : cat-ob(C)
11. y : cat-ob(C)
12. z : cat-ob(C)
13. g : cat-arrow(C) x (ob(T) y)
14. h : cat-arrow(C) y (ob(T) z)
⊢ (cat-comp(C) (ob(T) x) (ob(T) (ob(T) z)) (ob(T) z) 
   (arrow(T) x (ob(T) z) 
    (cat-comp(C) x (ob(T) y) (ob(T) z) g 
     (cat-comp(C) (ob(T) y) (ob(T) (ob(T) z)) (ob(T) z) (arrow(T) y (ob(T) z) h) (M3 z)))) 
   (M3 z))
= (cat-comp(C) (ob(T) x) (ob(T) y) (ob(T) z) 
   (cat-comp(C) (ob(T) x) (ob(T) (ob(T) y)) (ob(T) y) (arrow(T) x (ob(T) y) g) (M3 y)) 
   (cat-comp(C) (ob(T) y) (ob(T) (ob(T) z)) (ob(T) z) (arrow(T) y (ob(T) z) h) (M3 z)))
∈ (cat-arrow(C) (ob(T) x) (ob(T) z))

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[M:Monad(C)].  \mforall{}[x,y,z:cat-ob(C)].  \mforall{}[g:cat-arrow(C)  x  M(y)].  \mforall{}[h:cat-arrow(C)  y 
                                                                                                                                                                          M(z)].
    (monad-extend(C;M;x;z;cat-comp(C)  x  M(y)  M(z)  g  monad-extend(C;M;y;z;h))
    =  (cat-comp(C)  M(x)  M(y)  M(z)  monad-extend(C;M;x;y;g)  monad-extend(C;M;y;z;h)))


By

---

Latex:
(Auto
  THEN  DVar  `M'
  THEN  DProds
  THEN  DVar  `M2'
  THEN  DVar  `M3'
  THEN  (All  (RepUR  ``id\_functor  functor-comp  monad-extend  monad-fun``)
              THEN  All  (RepUR  ``monad-functor  monad-unit  monad-op``)
              )
  THEN  All  Reduce
  THEN  ExRepD)

---

Home Index