proposition: 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: Proof. exact (setquot_map_epi (λ x, idpath (h (setquotpr R x)))). Qed.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.ExactCategories.ExactCategories UniMath.Algebra.Groups UniMath.Algebra.Free_Monoids_and_Groups