`∀[C:SmallCategory]. ∀[M:Monad(C)].  (Kl(C;M) ∈ KlF(C;M) -| KlG(C;M))`

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

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

Date html generated: 2020_05_20-AM-08_00_03
Last ObjectModification: 2017_07_28-AM-09_21_10

Theory : small!categories

Home Index