---

Step * of Lemma monad-of-Kleisli-adjunction

∀[C:SmallCategory]. ∀[M:Monad(C)].  (adjMonad(Kl(C;M)) = M ∈ Monad(C))
BY
{ (Intros THEN BLemma `equal-monads` THEN Auto) }

1
1. C : SmallCategory
2. M : Monad(C)
⊢ monad-functor(adjMonad(Kl(C;M))) = monad-functor(M) ∈ Functor(C;C)

2
1. C : SmallCategory
2. M : Monad(C)
3. x : cat-ob(C)
⊢ 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))

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[M:Monad(C)].    (adjMonad(Kl(C;M))  =  M)


By

---

Latex:
(Intros  THEN  BLemma  `equal-monads`  THEN  Auto)

---

Home Index