proposition: Lemma free_monoid_extend_funcomp2 {X Y : hSet} {Z : monoid} (f: (X → free_monoid Y)) (g: (Y → Z)) : monoidfuncomp (free_monoid_extend f) (free_monoid_extend g) = free_monoid_extend (λ x, free_monoid_extend g (f x)).
proof: Proof. apply (invmaponpathsweq (invweq (free_monoid_universal_property _ _)) _ _). now apply idpath. Qed.
imports: UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.IteratedBinaryOperations UniMath.Combinatorics.Lists