Definition iseqclassconstr {X : UU} (R : hrel X) {A : hsubtype X} (ax0 : ishinh (carrier A)) (ax1 : ∏ x1 x2 : X, R x1 x2 -> A x1 -> A x2) (ax2 : ∏ x1 x2 : X, A x1 -> A x2 -> R x1 x2) : iseqclass R A := make_dirprod ax0 (make_dirprod ax1 ax2).
Require Import UniMath.Foundations.UnivalenceAxiom.