proposition: Lemma free_gr_extend_comp {X : hSet} {Y : gr} (g : monoidfun (free_gr X) Y): free_gr_extend (g ∘ free_gr_unit) ~ g.
proof: Proof. unfold homot. apply setquotunivprop'. - intro. apply (isasetmonoid Y). - intro l. refine (setquotunivcomm _ _ _ _ _ @ _). refine (_ @ (free_monoid_extend_comp (monoidfuncomp (free_gr_pr X) g)) l). apply (maponpaths iterop_list_mon). apply map_homot. intro x. induction x as [x|x]. + reflexivity. + simpl. refine (!monoidfuninvtoinv g _ @ _). reflexivity. Defined.
imports: UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.IteratedBinaryOperations UniMath.Combinatorics.Lists