proposition: Lemma presented_gr_extend_comp {X : hSet} {R : hrel (free_gr X)} {Y : gr} (g : monoidfun (presented_gr X R) Y) (H : iscomprelfun R (free_gr_extend (g ∘ presented_gr_intro))) : presented_gr_extend (g ∘ presented_gr_intro) H ~ g.
proof: Proof. unfold homot. apply setquotunivprop'. + intro. apply isasetmonoid. + intro x. refine (setquotunivcomm _ _ _ _ _ @ _). exact (free_gr_extend_comp (monoidfuncomp (presented_gr_pr R) g) _). Defined.
imports: UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.IteratedBinaryOperations UniMath.Combinatorics.Lists