Definition presented_grfun {X Y : hSet} {R : hrel (free_gr X)} {S : hrel (free_gr Y)} (f : X → Y) (H : iscomprelrelfun R S (free_grfun f)) : monoidfun (presented_gr X R) (presented_gr Y S). Proof. apply (presented_gr_extend (presented_gr_intro ∘ f)). intros x x' r. rewrite !(free_gr_extend_funcomp _ _ _). unfold funcomp. rewrite !(free_gr_extend_comp (presented_gr_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.