proposition: Lemma path_quotient_algebra_iff `{Univalence} (R : ∀ s x y, Φ s x y <-> Ψ s x y) : A/Φ = A/Ψ.
proof: Proof. apply path_quotient_algebra. funext s x y. refine (path_universe_uncurried _). apply equiv_iff_hprop; apply R. Defined.
imports: HoTT.Classes.interfaces.ua_congruence HSet Colimits.Quotient Classes.implementations.list Classes.interfaces.canonical_names Classes.theory.ua_homomorphism