Definition free_monoid_extend {X : hSet} {Y : monoid} (f : X → Y) : monoidfun (free_monoid X) Y. Proof. use monoidfunconstr. - intro l. exact (iterop_list_mon (map f l)). - use make_ismonoidfun. + intros l1 l2. refine (maponpaths _ (map_concatenate _ _ _) @ _). apply iterop_list_mon_concatenate. + reflexivity. Defined.
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.