proposition: Theorem issurjsetquotpr {X : UU} (R : eqrel X) : issurjective (setquotpr R).
proof: 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.
imports: UniMath.Foundations.Propositions