`{Univalence} (R : ∀ s x y, Φ s x y <-> Ψ s x y) : A/Φ = A/Ψ. Proof. apply path_quotient_algebra. funext s x y. refine (path_universe_uncurried _). apply equiv_iff_hprop; apply R. Defined.
Require Import Basics.Notations. Require Import Import algebra_notations ne_list.notations. Import quotient_algebra_notations.