---

Step * 1 2 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
⊢ (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))
BY
{ (RepUR ``adjunction-monad monad-functor mk-monad`` 0
   THEN RepUR ``Kleisli-left Kleisli-right functor-comp`` 0
   THEN Fold `monad-functor` 0) }

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
⊢ monad-extend(C;M;x;y;monad-unit(M;y) o 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
\mvdash{}  (arrow(monad-functor(adjMonad(Kl(C;M))))  x  y  f)  =  (arrow(monad-functor(M))  x  y  f)


By

---

Latex:
(RepUR  ``adjunction-monad  monad-functor  mk-monad``  0
  THEN  RepUR  ``Kleisli-left  Kleisli-right  functor-comp``  0
  THEN  Fold  `monad-functor`  0)

---

Home Index