Lemma free_gr_extend_comp {X : hSet} {Y : gr} (g : monoidfun (free_gr X) Y): free_gr_extend (g ∘ free_gr_unit) ~ g. 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.
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.