Definition monoid_axioms : eqsystem monoid_signature monoid_varspec := ⟦ 3 ⟧,, three_rec monoid_mul_assoc monoid_mul_lid monoid_mul_rid.
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Universal.EqAlgebras.