Definition weqneqh {X : UU} (is : isdeceq X) (x x' : X) : (x != x') ≃ (neqh is x x'). Proof. intros. unfold neqh. unfold booleq. apply weqimplimpl. - induction (is x x') as [ e | ne ]. + intro ne. induction (ne e). + intro ne'. simpl. apply idpath. - induction (is x x') as [ e | ne ]. + intro tf. induction (nopathstruetofalse tf). + intro. exact ne. - apply (isapropneg). - simpl. unfold isaprop. unfold isofhlevel. apply (isasetbool _ false). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.