Theorem isasetsetquot {X : UU} (R : hrel X) : isaset (setquot R). Proof. apply (isasetsubset (@pr1 _ _) (isasethsubtype X)). apply isinclpr1; intro x. apply isapropiseqclass. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.