Definition iseqrelconstr {X : UU} {R : hrel X} (trans0 : istrans R) (refl0 : isrefl R) (symm0 : issymm R) : iseqrel R := make_dirprod (make_dirprod trans0 refl0) symm0.
Require Import UniMath.Foundations.UnivalenceAxiom.