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. intro; apply map_compose. 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.