proposition: Lemma sfmap_as_bind_ret `{Equiv A} `{Equiv B} `{!Setoid_Morphism (f : A → B)} : sfmap f = bind (ret ∘ f).
proof: Proof. pose proof (setoidmor_a f). pose proof (setoidmor_b f). rewrite bind_as_join_sfmap. rewrite sfmap_comp. rewrite <-compose_assoc. rewrite join_sfmap_ret. now apply setoids.ext_equiv_refl. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.functors