Definition setquot2pr {X : UU} (R : hrel X) : X -> setquot2 R := λ x : X, make_image (compevmapset R) _ (hinhpr (make_hfiber (compevmapset R) x (idpath _))).
Require Import UniMath.Foundations.UnivalenceAxiom.