Lemma setquot_map_recovery {X : Type} (R : eqrel X) (Y : hSet) (h : setquot R → Y) : ∏ w, setquotuniv R Y (h ∘ setquotpr R) (λ x x' (r : R x x'), maponpaths h (iscompsetquotpr R x x' r)) w = h w. Proof. exact (setquot_map_epi (λ x, idpath (h (setquotpr R x)))). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Free_Monoids_and_Groups.