Homomorphism (A/Φ) B → {f : Homomorphism A B | ∀ s (x y : A s), Φ s x y → f s x = f s y}. 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.
Require Import Basics.Notations. Require Import Import algebra_notations ne_list.notations. Import quotient_algebra_notations.