Definition presented_gr_universal_property {X : hSet} (R : hrel (free_gr X)) (Y : gr) : monoidfun (presented_gr X R) Y ≃ ∑(f : X → Y), iscomprelfun R (free_gr_extend f). Proof. use weq_iso. - intro g. exact (tpair _ (g ∘ presented_gr_intro) (iscomprelfun_presented_grfun g)). - intro f. exact (presented_gr_extend (pr1 f) (pr2 f)). - intro g. apply monoidfun_paths, funextfun, presented_gr_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.