Definition free_gr_extend {X : hSet} {Y : gr} (f : X → Y) : monoidfun (free_gr X) Y. Proof. use presented_monoid_extend. - exact (sumofmaps f (grinv Y ∘ f)). - unfold iscomprelfun. apply free_gr_hrel_univ. + intros x y. apply (isasetmonoid Y). + intro x. induction x as [x|x]. * apply (grrinvax Y (f x)). * apply (grlinvax Y (f x)). 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.