`∀[C:SmallCategory]. ∀[M:Monad(C)].  (adjMonad(Kl(C;M)) = M ∈ Monad(C))`

Proof

Definitions occuring in Statement :  Kleisli-adjunction: `Kl(C;M)` Kleisli-right: `KlG(C;M)` Kleisli-left: `KlF(C;M)` Kleisli-cat: `Kl(C;M)` adjunction-monad: `adjMonad(adj)` cat-monad: `Monad(C)` small-category: `SmallCategory` uall: `∀[x:A]. B[x]` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` uimplies: `b supposing a` monad-unit: `monad-unit(M;x)` pi1: `fst(t)` pi2: `snd(t)` adjunction-monad: `adjMonad(adj)` mk-monad: mk-monad Kleisli-adjunction: `Kl(C;M)` mk-adjunction: `mk-adjunction(b.eps[b];a.eta[a])` mk-nat-trans: `x |→ T[x]` monad-functor: `monad-functor(M)` Kleisli-right: `KlG(C;M)` Kleisli-left: `KlF(C;M)` functor-comp: `functor-comp(F;G)` top: `Top` so_lambda: so_lambda3 so_apply: `x[s1;s2;s3]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` monad-fun: `M(x)` cat_comp: `g o f` monad-extend: `monad-extend(C;M;x;y;f)` subtype_rel: `A ⊆r B` true: `True` squash: `↓T` prop: `ℙ` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` monad-op: `monad-op(M;x)`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination hypothesis independent_isectElimination lambdaFormation sqequalRule because_Cache applyEquality isect_memberEquality voidElimination voidEquality lambdaEquality natural_numberEquality imageElimination equalityTransitivity equalitySymmetry universeEquality imageMemberEquality baseClosed productElimination independent_functionElimination

Latex: