fact: Definition iseqclass {X : UU} (R : hrel X) (A : hsubtype X) : UU := dirprod (ishinh (carrier A)) (dirprod (∏ x1 x2 : X, R x1 x2 -> A x1 -> A x2) (∏ x1 x2 : X, A x1 -> A x2 -> R x1 x2)).
imports: UniMath.Foundations.Propositions