fact: Definition make_eqalgebra {σ : eqspec} (a : algebra σ) (H : is_eqalgebra a) : eqalgebra σ := tpair is_eqalgebra a H.
imports: UniMath.MoreFoundations.Notations UniMath.Algebra.Universal.Algebras UniMath.Algebra.Universal.Equations