proposition: Lemma join_as_bind `{Setoid A} : join = bind id.
proof: Proof. rewrite bind_as_join_sfmap. rewrite sfmap_id. now apply setoids.ext_equiv_refl. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.functors