proposition: Lemma free_abmonoid_extend_homot {X : hSet} {Y : abmonoid} {f f' : X → Y} (h : f ~ f') : free_abmonoid_extend f ~ free_abmonoid_extend f'.
proof: Proof. unfold homot. apply setquotunivprop'. - intro x. apply isasetmonoid. - exact (free_monoid_extend_homot h). Defined.
imports: UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.IteratedBinaryOperations UniMath.Combinatorics.Lists