proposition: Lemma ump_quotient_algebra_lr : {f : Homomorphism A B | ∀ s (x y : A s), Φ s x y → f s x = f s y} → Homomorphism (A/Φ) B.
proof: Proof. intros [f P]. exists (hom_quotient_algebra_mapout f P). exact _. Defined.
imports: HoTT.Classes.interfaces.ua_congruence HSet Colimits.Quotient Classes.implementations.list Classes.interfaces.canonical_names Classes.theory.ua_homomorphism