`∀[A,B:SmallCategory]. ∀[F:Functor(A;B)]. ∀[G:Functor(B;A)]. ∀[adj:F -| G].  (adjMonad(adj) ∈ Monad(A))`

Proof

Definitions occuring in Statement :  adjunction-monad: `adjMonad(adj)` cat-monad: `Monad(C)` counit-unit-adjunction: `F -| G` cat-functor: `Functor(C1;C2)` small-category: `SmallCategory` uall: `∀[x:A]. B[x]` member: `t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` adjunction-monad: `adjMonad(adj)` member: `t ∈ T` counit-unit-adjunction: `F -| G` pi2: `snd(t)` pi1: `fst(t)` uimplies: `b supposing a` all: `∀x:A. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` nat-trans: `nat-trans(C;D;F;G)` id_functor: `1` functor-comp: `functor-comp(F;G)` top: `Top` so_lambda: so_lambda3 so_apply: `x[s1;s2;s3]` counit-unit-equations: `counit-unit-equations(D;C;F;G;eps;eta)` and: `P ∧ Q` true: `True` squash: `↓T` prop: `ℙ` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q`
Lemmas referenced :  mk-monad_wf functor-comp_wf counit-unit-adjunction_wf cat-functor_wf small-category_wf cat-ob_wf mk-nat-trans_wf ob_mk_functor_lemma arrow_mk_functor_lemma functor-arrow_wf functor-ob_wf cat-arrow_wf cat-comp_wf equal_wf squash_wf true_wf functor-arrow-comp iff_weakening_equal ap_mk_nat_trans_lemma cat-id_wf functor-arrow-id
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename sqequalRule productElimination independent_isectElimination because_Cache dependent_functionElimination lambdaEquality isect_memberEquality voidElimination voidEquality applyEquality functionExtensionality lambdaFormation natural_numberEquality imageElimination equalityTransitivity equalitySymmetry universeEquality imageMemberEquality baseClosed independent_functionElimination

Latex:
\mforall{}[A,B:SmallCategory].  \mforall{}[F:Functor(A;B)].  \mforall{}[G:Functor(B;A)].  \mforall{}[adj:F  -|  G].