---

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


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))
BY
{ (RW CatNormC 0 THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  M  :  Monad(C)
3.  x  :  cat-ob(C)@i
\mvdash{}  (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)


By

---

Latex:
(RW  CatNormC  0  THEN  Auto)

---

Home Index