fact: Definition monoid_signature := make_signature_simple_single_sorted [2; 0].
imports: UniMath.MoreFoundations.Notations UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Monoids UniMath.Algebra.Universal.EqAlgebras