---

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


1. C : SmallCategory
2. M : Monad(C)
⊢ monad-functor(adjMonad(Kl(C;M))) = monad-functor(M) ∈ Functor(C;C)
BY
{ (BLemma `equal-functors` THEN Auto) }

1
1. C : SmallCategory
2. M : Monad(C)
3. x : cat-ob(C)
⊢ (ob(monad-functor(adjMonad(Kl(C;M)))) x) = (ob(monad-functor(M)) x) ∈ cat-ob(C)

2
1. C : SmallCategory
2. M : Monad(C)
3. x : cat-ob(C)
4. y : cat-ob(C)
5. f : cat-arrow(C) x y
⊢ (arrow(monad-functor(adjMonad(Kl(C;M)))) x y f)
= (arrow(monad-functor(M)) x y f)
∈ (cat-arrow(C) (ob(monad-functor(adjMonad(Kl(C;M)))) x) (ob(monad-functor(adjMonad(Kl(C;M)))) y))

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  M  :  Monad(C)
\mvdash{}  monad-functor(adjMonad(Kl(C;M)))  =  monad-functor(M)


By

---

Latex:
(BLemma  `equal-functors`  THEN  Auto)

---

Home Index