Definition presented_monoid_universal_property {X : hSet} (R : hrel (free_monoid X)) (Y : monoid) : monoidfun (presented_monoid X R) Y ≃ ∑(f : X → Y), iscomprelfun R (free_monoid_extend f). Proof. use weq_iso. - intro g. exact (tpair _ (g ∘ presented_monoid_intro) (iscomprelfun_presented_monoidfun g)). - intro f. exact (presented_monoid_extend (pr1 f) (pr2 f)). - intro g. apply monoidfun_paths, funextfun, presented_monoid_extend_comp. - intro f. use total2_paths_f. + apply funextfun. intro x. reflexivity. + apply isapropiscomprelfun. 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.