Theorem isasetsetquot2 {X : UU} (R : hrel X) : isaset (setquot2 R). Proof. intros. assert (is1: isofhlevel 2 (∏ S : hSet, (compfun R S) -> S)). { apply impred. intro. apply impred. intro X0. apply (pr2 t). } apply (isasetsubset _ is1 (isinclpr1image _)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.