Step
*
1
1
of Lemma
monad-of-Kleisli-adjunction
1. C : SmallCategory
2. M : Monad(C)
3. x : cat-ob(C)
⊢ (ob(monad-functor(adjMonad(Kl(C;M)))) x) = (ob(monad-functor(M)) x) ∈ cat-ob(C)
BY
{ (RepUR ``adjunction-monad monad-functor mk-monad`` 0
   THEN RepUR ``Kleisli-left Kleisli-right functor-comp`` 0
   THEN Fold `monad-functor` 0
   THEN Fold `monad-fun` 0
   THEN Auto) }
Latex:
Latex:
1.  C  :  SmallCategory
2.  M  :  Monad(C)
3.  x  :  cat-ob(C)
\mvdash{}  (ob(monad-functor(adjMonad(Kl(C;M))))  x)  =  (ob(monad-functor(M))  x)
By
Latex:
(RepUR  ``adjunction-monad  monad-functor  mk-monad``  0
  THEN  RepUR  ``Kleisli-left  Kleisli-right  functor-comp``  0
  THEN  Fold  `monad-functor`  0
  THEN  Fold  `monad-fun`  0
  THEN  Auto)
Home
Index