Definition monoid_algebra (M: monoid) : algebra monoid_signature := make_algebra_simple_single_sorted' monoid_signature M [( op ; unel M )].
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Universal.EqAlgebras.