proposition: Lemma setquot_map_epi {X : Type} {R : eqrel X} {Y : hSet} {h h' : setquot R → Y} : h ∘ setquotpr R ~ h' ∘ setquotpr R -> h ~ h'.
proof: Proof. use (surjectionisepitosets _ _ _ (issurjsetquotpr R) (setproperty Y)). Defined.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.ExactCategories.ExactCategories UniMath.Algebra.Groups UniMath.Algebra.Free_Monoids_and_Groups