Definition is_eqalgebra_monoid : is_eqalgebra (σ := monoid_eqspec) (monoid_algebra M). Proof. red. simpl. apply three_rec_dep; cbn. - exact holds_monoid_mul_assoc. - exact holds_monoid_mul_lid. - exact holds_monoid_mul_rid. Defined.
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Universal.EqAlgebras.