Lemma free_abgr_extend_homot {X : hSet} {Y : abgr} {f f' : X → Y} (h : f ~ f') : free_abgr_extend f ~ free_abgr_extend f'. Proof. unfold homot. apply setquotunivprop'. - intro x. apply isasetmonoid. - exact (free_gr_extend_homot h). 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.