Definition setquot_universal_property (X:Type) (R:eqrel X) (Y:hSet) : (setquot R -> Y) ≃ (∑ f : X -> Y, iscomprelfun R f). Proof. use weq_iso. - intros h. exists (h ∘ setquotpr R). intros x x' r. simpl. apply maponpaths. apply iscompsetquotpr. exact r. - intros f. exact (setquotuniv R Y (pr1 f) (pr2 f)). - intros h. apply funextsec. unfold pr1,pr2. intros w. apply setquot_map_recovery. - intros f. cbn beta. apply subtypePath. * intros f'. apply isapropiscomprelfun. * cbn. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Free_Monoids_and_Groups.