Definition eqax2 {X : UU} {R : hrel X} {A : hsubtype X} : iseqclass R A -> ∏ x1 x2 : X, A x1 -> A x2 -> R x1 x2 := λ is : iseqclass R A, pr2 (pr2 is).
Require Import UniMath.Foundations.UnivalenceAxiom.