proposition: Lemma strong_binary_setoid_morphism_commutative {f : A -> A -> B} `{!Commutative f} `{forall z, StrongExtensionality (f z)} : StrongBinaryExtensionality f.
proof: Proof. apply @strong_binary_setoid_morphism_both_coordinates;try apply _. intros z x y. rewrite !(commutativity _ z). apply (strong_extensionality (f z)). Qed.
imports: HoTT.Classes.interfaces.abstract_algebra