Definition free_monoid_universal_property (X : hSet) (Y : monoid) : (X → Y) ≃ monoidfun (free_monoid X) Y. Proof. use weq_iso. - apply free_monoid_extend. - intro g. exact (g ∘ free_monoid_unit). - intro f. apply funextfun. intro x. reflexivity. - intro g. apply monoidfun_paths. apply funextfun. exact (free_monoid_extend_comp g). 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.