Definition free_gr_universal_property (X : hSet) (Y : gr) : (X → Y) ≃ monoidfun (free_gr X) Y. Proof. use weq_iso. - apply free_gr_extend. - intro g. exact (g ∘ free_gr_unit). - intro f. apply funextfun. intro x. reflexivity. - intro g. apply monoidfun_paths, funextfun, free_gr_extend_comp. 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.