Definition presented_abgr_extend {X : hSet} {R : hrel (free_abgr X)} {Y : abgr} (f : X → Y) (H : iscomprelfun R (free_abgr_extend f)) : monoidfun (presented_abgr X R) Y. Proof. use monoidquotuniv. - exact (free_abgr_extend f). - exact (iscomprelfun_generated_binopeqrel _ H). 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.