---

Step * 1 2 1 1 1 1 of Lemma monad-of-Kleisli-adjunction


1. C : SmallCategory
2. M : Monad(C)
3. x : cat-ob(C)
4. y : cat-ob(C)
5. f : cat-arrow(C) x y
6. ∀[x:cat-ob(C)]
     ((((cat-comp(C) M(x) M(M(x)) M(x) monad-unit(M;M(x)) monad-op(M;x)) = (cat-id(C) M(x)) ∈ (cat-arrow(C) M(x) M(x)))
     ∧ ((cat-comp(C) M(x) M(M(x)) M(x) (arrow(monad-functor(M)) x M(x) monad-unit(M;x)) monad-op(M;x))
       = (cat-id(C) M(x))
       ∈ (cat-arrow(C) M(x) M(x))))
     ∧ ((cat-comp(C) M(M(M(x))) M(M(x)) M(x) monad-op(M;M(x)) monad-op(M;x))
       = (cat-comp(C) M(M(M(x))) M(M(x)) M(x) (arrow(monad-functor(M)) M(M(x)) M(x) monad-op(M;x)) monad-op(M;x))
       ∈ (cat-arrow(C) M(M(M(x))) M(x))))
⊢ (cat-comp(C) M(x) M(M(y)) M(y) 
   (cat-comp(C) M(x) M(y) M(M(y)) (arrow(monad-functor(M)) x y f) (arrow(monad-functor(M)) y M(y) monad-unit(M;y))) 
   monad-op(M;y))
= (arrow(monad-functor(M)) x y f)
∈ (cat-arrow(C) M(x) M(y))
BY
{ All (Fold `cat_comp`) }

1
1. C : SmallCategory
2. M : Monad(C)
3. x : cat-ob(C)
4. y : cat-ob(C)
5. f : cat-arrow(C) x y
6. ∀[x:cat-ob(C)]
     (((monad-op(M;x) o monad-unit(M;M(x)) = (cat-id(C) M(x)) ∈ (cat-arrow(C) M(x) M(x)))
     ∧ (monad-op(M;x) o arrow(monad-functor(M)) x M(x) monad-unit(M;x) = (cat-id(C) M(x)) ∈ (cat-arrow(C) M(x) M(x))))
     ∧ (monad-op(M;x) o monad-op(M;M(x))
       = monad-op(M;x) o arrow(monad-functor(M)) M(M(x)) M(x) monad-op(M;x)
       ∈ (cat-arrow(C) M(M(M(x))) M(x))))
⊢ monad-op(M;y) o arrow(monad-functor(M)) y M(y) monad-unit(M;y) o arrow(monad-functor(M)) x y f
= (arrow(monad-functor(M)) x y f)
∈ (cat-arrow(C) M(x) M(y))

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  M  :  Monad(C)
3.  x  :  cat-ob(C)
4.  y  :  cat-ob(C)
5.  f  :  cat-arrow(C)  x  y
6.  \mforall{}[x:cat-ob(C)]
          ((((cat-comp(C)  M(x)  M(M(x))  M(x)  monad-unit(M;M(x))  monad-op(M;x))  =  (cat-id(C)  M(x)))
          \mwedge{}  ((cat-comp(C)  M(x)  M(M(x))  M(x)  (arrow(monad-functor(M))  x  M(x)  monad-unit(M;x)) 
                  monad-op(M;x))
              =  (cat-id(C)  M(x))))
          \mwedge{}  ((cat-comp(C)  M(M(M(x)))  M(M(x))  M(x)  monad-op(M;M(x))  monad-op(M;x))
              =  (cat-comp(C)  M(M(M(x)))  M(M(x))  M(x)  (arrow(monad-functor(M))  M(M(x))  M(x)  monad-op(M;x)) 
                    monad-op(M;x))))
\mvdash{}  (cat-comp(C)  M(x)  M(M(y))  M(y) 
      (cat-comp(C)  M(x)  M(y)  M(M(y))  (arrow(monad-functor(M))  x  y  f) 
        (arrow(monad-functor(M))  y  M(y)  monad-unit(M;y))) 
      monad-op(M;y))
=  (arrow(monad-functor(M))  x  y  f)


By

---

Latex:
All  (Fold  `cat\_comp`)

---

Home Index