Theorem issurjsetquotpr {X : UU} (R : eqrel X) : issurjective (setquotpr R). Proof. intros. unfold issurjective. intro c. apply (@hinhuniv (carrier (pr1 c))). intro x. apply hinhpr. split with (pr1 x). - apply setquotl0. - apply (eqax0 (pr2 c)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.