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. apply (invmaponpathsweq (invweq (free_monoid_universal_property _ _)) _ _). now apply idpath. Qed.
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.