`∀[C:SmallCategory]. ∀[M1,M2:Monad(C)].`
`  (M1 = M2 ∈ Monad(C)) supposing `
`     ((∀x:cat-ob(C). (monad-op(M1;x) = monad-op(M2;x) ∈ (cat-arrow(C) M1(M1(x)) M1(x)))) and `
`     (∀x:cat-ob(C). (monad-unit(M1;x) = monad-unit(M2;x) ∈ (cat-arrow(C) x M1(x)))) and `
`     (monad-functor(M1) = monad-functor(M2) ∈ Functor(C;C)))`

Proof

Definitions occuring in Statement :  monad-op: `monad-op(M;x)` monad-unit: `monad-unit(M;x)` monad-fun: `M(x)` monad-functor: `monad-functor(M)` cat-monad: `Monad(C)` cat-functor: `Functor(C1;C2)` cat-arrow: `cat-arrow(C)` cat-ob: `cat-ob(C)` small-category: `SmallCategory` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` apply: `f a` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` monad-fun: `M(x)` all: `∀x:A. B[x]` member: `t ∈ T` squash: `↓T` prop: `ℙ` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` cat-monad: `Monad(C)` spreadn: spread3 nat-trans: `nat-trans(C;D;F;G)` functor-comp: `functor-comp(F;G)` top: `Top` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` id_functor: `1` monad-op: `monad-op(M;x)` pi2: `snd(t)` monad-functor: `monad-functor(M)` pi1: `fst(t)` monad-unit: `monad-unit(M;x)` mk-functor: mk-functor functor-ob: `ob(F)`
Lemmas referenced :  equal_wf squash_wf true_wf istype-universe cat-ob_wf functor-ob_wf cat-functor_wf monad-functor_wf subtype_rel_self iff_weakening_equal ob_mk_functor_lemma istype-void arrow_mk_functor_lemma cat-arrow_wf cat-comp_wf cat-id_wf functor-arrow_wf monad-fun_wf monad-op_wf subtype_rel-equal monad-unit_wf cat-monad_wf small-category_wf nat-trans_wf id_functor_wf functor-comp_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut sqequalRule lambdaFormation_alt applyEquality thin lambdaEquality_alt sqequalHypSubstitution imageElimination introduction extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry universeIsType inhabitedIsType instantiate universeEquality because_Cache natural_numberEquality imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination setElimination rename dependent_set_memberEquality_alt dependent_functionElimination isect_memberEquality_alt voidElimination productIsType functionIsType equalityIsType1 dependent_pairEquality_alt independent_pairEquality lambdaEquality functionExtensionality voidEquality isect_memberEquality

Latex:
(M1  =  M2)  supposing