Algebra σ := BuildAlgebra carriers_quotient_algebra ops_quotient_algebra. Global Instance hset_quotient_algebra : IsHSetAlgebra . Proof. intro s. exact _. Qed.
Require Import Basics.Notations. Require Import Import algebra_notations ne_list.notations. Import quotient_algebra_notations.