Homomorphism A (A/Φ) := BuildHomomorphism def_hom_quotient. Global Instance surjection_quotient : ∀ s, IsSurjection ( s). Proof. intro s. apply issurj_class_of. Qed.
Require Import Basics.Notations. Require Import Import algebra_notations ne_list.notations. Import quotient_algebra_notations.