Definition presented_monoidfun {X Y : hSet} {R : hrel (free_monoid X)} {S : hrel (free_monoid Y)} (f : X → Y) (H : iscomprelrelfun R S (free_monoidfun f)) : monoidfun (presented_monoid X R) (presented_monoid Y S). Proof. apply (presented_monoid_extend (presented_monoid_intro ∘ f)). intros x x' r. rewrite !free_monoid_extend_funcomp. unfold funcomp. rewrite !(free_monoid_extend_comp (presented_monoid_pr S)). apply iscompsetquotpr. apply generated_binopeqrel_intro. exact (H x x' 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.