proposition: Lemma free_gr_extend_homot {X : hSet} {Y : gr} {f f' : X → Y} (h : f ~ f') : free_gr_extend f ~ free_gr_extend f'.
proof: Proof. unfold homot. apply setquotunivprop'. - intro x. apply isasetmonoid. - refine (free_monoid_extend_homot _). apply sumofmaps_homot. + exact h. + intro x. exact (maponpaths (grinv Y) (h x)). Defined.
imports: UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.IteratedBinaryOperations UniMath.Combinatorics.Lists