(g : Homomorphism (A/Φ) B) : Homomorphism A B := hom_compose g (hom_quotient Φ).
Require Import Basics.Notations. Require Import Import algebra_notations ne_list.notations. Import quotient_algebra_notations.