---

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


1. C : SmallCategory
2. M : Monad(C)
3. x : cat-ob(C)@i
4. y : cat-ob(C)@i
5. f : cat-arrow(C) x y@i
⊢ monad-extend(C;M;x;y;monad-unit(M;y) o f) = (monad-functor(M) x y f) ∈ (cat-arrow(C) M(x) M(y))
BY
{ RepUR ``monad-extend cat_comp`` 0 }

1
1. C : SmallCategory
2. M : Monad(C)
3. x : cat-ob(C)@i
4. y : cat-ob(C)@i
5. f : cat-arrow(C) x y@i
⊢ (cat-comp(C) M(x) M(M(y)) M(y) (monad-functor(M) x M(y) (cat-comp(C) x y M(y) f monad-unit(M;y))) monad-op(M;y))
= (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)@i
4.  y  :  cat-ob(C)@i
5.  f  :  cat-arrow(C)  x  y@i
\mvdash{}  monad-extend(C;M;x;y;monad-unit(M;y)  o  f)  =  (monad-functor(M)  x  y  f)


By

---

Latex:
RepUR  ``monad-extend  cat\_comp``  0

---

Home Index