---

Step * of Lemma Kleisli-adjunction_wf

∀[C:SmallCategory]. ∀[M:Monad(C)].  (Kl(C;M) ∈ KlF(C;M) -| KlG(C;M))
BY
{ (ProveWfLemma
   THEN RepUR ``Kleisli-cat Kleisli-left Kleisli-right mk-cat`` 0
   THEN RepUR ``counit-unit-equations cat_comp`` 0
   THEN Auto) }

1
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))

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[M:Monad(C)].    (Kl(C;M)  \mmember{}  KlF(C;M)  -|  KlG(C;M))


By

---

Latex:
(ProveWfLemma
  THEN  RepUR  ``Kleisli-cat  Kleisli-left  Kleisli-right  mk-cat``  0
  THEN  RepUR  ``counit-unit-equations  cat\_comp``  0
  THEN  Auto)

---

Home Index