proposition: Lemma iscomprelfun_presented_abmonoidfun {X : hSet} {R : hrel (free_abmonoid X)} {Y : abmonoid} (g : monoidfun (presented_abmonoid X R) Y) : iscomprelfun R (free_abmonoid_extend (g ∘ presented_abmonoid_intro)).
proof: Proof. intros x x' r. rewrite !(free_abmonoid_extend_comp (monoidfuncomp (presented_abmonoid_pr R) g)). apply (maponpaths (pr1 g)). apply iscompsetquotpr. exact (generated_binopeqrel_intro r). Defined.
imports: UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.IteratedBinaryOperations UniMath.Combinatorics.Lists