---

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


1. C : SmallCategory
2. M : Monad(C)
3. x : cat-ob(C)@i
⊢ monad-op(adjMonad(Kl(C;M));x)
= monad-op(M;x)
∈ (cat-arrow(C) adjMonad(Kl(C;M))(adjMonad(Kl(C;M))(x)) adjMonad(Kl(C;M))(x))
BY
{ ((RepUR ``adjunction-monad Kleisli-adjunction mk-adjunction`` 0 THEN RepUR ``monad-functor mk-monad monad-op`` 0)
   THEN (RepUR ``Kleisli-left Kleisli-right functor-comp`` 0 THEN RepUR ``monad-extend monad-fun monad-functor`` 0)
   THEN Try (Folds ``monad-op monad-functor`` 0)
   THEN Fold `monad-fun` 0) }

1
1. C : SmallCategory
2. M : Monad(C)
3. x : cat-ob(C)@i
⊢ (cat-comp(C) M(M(x)) M(M(x)) M(x) (monad-functor(M) M(x) M(x) (cat-id(C) M(x))) monad-op(M;x))
= monad-op(M;x)
∈ (cat-arrow(C) M(M(x)) M(x))

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  M  :  Monad(C)
3.  x  :  cat-ob(C)@i
\mvdash{}  monad-op(adjMonad(Kl(C;M));x)  =  monad-op(M;x)


By

---

Latex:
((RepUR  ``adjunction-monad  Kleisli-adjunction  mk-adjunction``  0
    THEN  RepUR  ``monad-functor  mk-monad  monad-op``  0
    )
  THEN  (RepUR  ``Kleisli-left  Kleisli-right  functor-comp``  0
              THEN  RepUR  ``monad-extend  monad-fun  monad-functor``  0
              )
  THEN  Try  (Folds  ``monad-op  monad-functor``  0)
  THEN  Fold  `monad-fun`  0)

---

Home Index