Definition eqrelconstr {X : UU} (R : hrel X) (is1 : istrans R) (is2 : isrefl R) (is3 : issymm R) : eqrel X := make_eqrel R (make_dirprod (make_dirprod is1 is2) is3).
Require Import UniMath.Foundations.UnivalenceAxiom.