proposition: Lemma bind_twice `{Equiv A} `{Equiv B} `{Setoid C} `{!Setoid_Morphism (f : B → M C)} `{!Setoid_Morphism (g : A → M B)} : bind (bind f) = bind f ∘ join.
proof: Proof. pose proof (setoidmor_a f). pose proof (setoidmor_b f). pose proof (setoidmor_b g). rewrite join_as_bind. rewrite bind_assoc. now apply setoids.ext_equiv_refl. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.functors