Definition free_monoid (X : hSet) : monoid := make_monoid (make_setwithbinop (make_hSet (list X) (isofhlevellist 0 (pr2 X))) _) (ismonoidop_concatenate X).
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Combinatorics.Lists.