proposition: Lemma free_monoidfun_comp_homot {X Y Z : hSet} (f : X -> Y) (g : Y -> Z) : (free_monoidfun (g ∘ f)) ~ free_monoidfun g ∘ free_monoidfun f.
proof: Proof. intro; apply map_compose. Qed.
imports: UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.IteratedBinaryOperations UniMath.Combinatorics.Lists