### Nuprl Lemma : Kleisli-right_wf

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

Proof

Definitions occuring in Statement :  Kleisli-right: `KlG(C;M)` Kleisli-cat: `Kl(C;M)` cat-monad: `Monad(C)` cat-functor: `Functor(C1;C2)` small-category: `SmallCategory` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` Kleisli-right: `KlG(C;M)` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` cat-ob: `cat-ob(C)` pi1: `fst(t)` Kleisli-cat: `Kl(C;M)` mk-cat: mk-cat so_apply: `x[s]` so_lambda: so_lambda3 cat-arrow: `cat-arrow(C)` pi2: `snd(t)` so_apply: `x[s1;s2;s3]` top: `Top` squash: `↓T` prop: `ℙ` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination hypothesis because_Cache lambdaEquality applyEquality independent_isectElimination isect_memberEquality voidElimination voidEquality imageElimination equalityTransitivity equalitySymmetry universeEquality natural_numberEquality imageMemberEquality baseClosed productElimination independent_functionElimination axiomEquality

Latex: