proposition: Lemma path_quotient_algebra `{Funext} (p : Φ = Ψ) : A/Φ = A/Ψ.
proof: Proof. by destruct p, (path_ishprop CΦ CΨ). Defined.
imports: HoTT.Classes.interfaces.ua_congruence HSet Colimits.Quotient Classes.implementations.list Classes.interfaces.canonical_names Classes.theory.ua_homomorphism