{f : Homomorphism A B | ∀ s (x y : A s), Φ s x y → f s x = f s y} → Homomorphism (A/Φ) B. Proof. intros [f P]. exists (hom_quotient_algebra_mapout f P). exact _. Defined.
Require Import Basics.Notations. Require Import Import algebra_notations ne_list.notations. Import quotient_algebra_notations.