Lemma presented_abgr_extend_comp {X : hSet} {R : hrel (free_abgr X)} {Y : abgr} (g : monoidfun (presented_abgr X R) Y) (H : iscomprelfun R (free_abgr_extend (g ∘ presented_abgr_intro))) : presented_abgr_extend (g ∘ presented_abgr_intro) H ~ g. Proof. unfold homot. apply setquotunivprop'. + intro. apply isasetmonoid. + intro x. refine (setquotunivcomm _ _ _ _ _ @ _). exact (free_abgr_extend_comp (monoidfuncomp (presented_abgr_pr R) g) x). 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.