{f : Homomorphism A B | ∀ s (x y : A s), Φ s x y → f s x = f s y} <~> Homomorphism (A/Φ) B. Proof. apply (equiv_adjointify ump_quotient_algebra_lr ump_quotient_algebra_rl). - intro G. apply path_hset_homomorphism. funext s. exact (eissect (equiv_quotient_ump (Φ s) _) (G s)). - intro F. apply path_sigma_hprop. by apply path_hset_homomorphism. Defined.
Require Import Basics.Notations. Require Import Import algebra_notations ne_list.notations. Import quotient_algebra_notations.