Lemma iscomprelfun_presented_monoidfun {X : hSet} {R : hrel (free_monoid X)} {Y : monoid} (g : monoidfun (presented_monoid X R) Y) : iscomprelfun R (free_monoid_extend (g ∘ presented_monoid_intro)). Proof. intros x x' r. rewrite !(free_monoid_extend_comp (monoidfuncomp (presented_monoid_pr R) g)). apply (maponpaths (pr1 g)). apply iscompsetquotpr. exact (generated_binopeqrel_intro r). 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.