proposition: Lemma ump_quotient_algebra_rl : Homomorphism (A/Φ) B → {f : Homomorphism A B | ∀ s (x y : A s), Φ s x y → f s x = f s y}.
proof: Proof. intro g. exists (hom_quotient_algebra_mapin g). intros s x y E. exact (transport (λ z, g s (class_of (Φ s) x) = g s z) (qglue E) idpath). Defined.
imports: HoTT.Classes.interfaces.ua_congruence HSet Colimits.Quotient Classes.implementations.list Classes.interfaces.canonical_names Classes.theory.ua_homomorphism