Lemma isapropiseqclass {X : UU} (R : hrel X) (A : hsubtype X) : isaprop (iseqclass R A). Proof. apply isofhleveldirprod. - exact (isapropishinh (carrier A)). - apply isofhleveldirprod. + repeat (apply impred; intro). exact (pr2 (A t0)). + repeat (apply impred; intro). exact (pr2 (R t t0)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.