fact: Definition def_hom_quotient : ∀ (s : Sort σ), A s → (A/Φ) s := λ s x, class_of (Φ s) x.
imports: HoTT.Classes.interfaces.ua_congruence HSet Colimits.Quotient Classes.implementations.list Classes.interfaces.canonical_names Classes.theory.ua_homomorphism