---

Step * 1 of Lemma Kleisli-adjunction_wf


1. C : SmallCategory
2. M : Monad(C)
3. b1 : cat-ob(Kl(C;M))
4. b2 : cat-ob(Kl(C;M))
5. g : cat-arrow(Kl(C;M)) b1 b2
⊢ (cat-comp(C) M(b1) M(b1) M(b2) (cat-id(C) M(b1)) monad-extend(C;M;b1;b2;g))
= (cat-comp(C) M(b1) M(M(b2)) M(b2) (cat-comp(C) M(b1) M(b2) M(M(b2)) monad-extend(C;M;b1;b2;g) monad-unit(M;M(b2))) 
   monad-extend(C;M;M(b2);b2;cat-id(C) M(b2)))
∈ (cat-arrow(C) M(b1) M(b2))
BY
{ (RWW "cat-comp-assoc monad-unit-extend" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  M  :  Monad(C)
3.  b1  :  cat-ob(Kl(C;M))
4.  b2  :  cat-ob(Kl(C;M))
5.  g  :  cat-arrow(Kl(C;M))  b1  b2
\mvdash{}  (cat-comp(C)  M(b1)  M(b1)  M(b2)  (cat-id(C)  M(b1))  monad-extend(C;M;b1;b2;g))
=  (cat-comp(C)  M(b1)  M(M(b2))  M(b2) 
      (cat-comp(C)  M(b1)  M(b2)  M(M(b2))  monad-extend(C;M;b1;b2;g)  monad-unit(M;M(b2))) 
      monad-extend(C;M;M(b2);b2;cat-id(C)  M(b2)))


By

---

Latex:
(RWW  "cat-comp-assoc  monad-unit-extend"  0  THEN  Auto)

---

Home Index