Homomorphism (A/Ψ) (A/Φ) := BuildHomomorphism def_third_surjection. Global Instance surjection_third_surjection (s : Sort σ) : IsSurjection ( s). Proof. apply BuildIsSurjection. refine (Quotient_ind_hprop (Φ s) _ _). intro x. apply tr. by exists (class_of (Ψ s) x). Qed.
Require Import Import algebra_notations quotient_algebra_notations isomorphic_notations.