Definition weqeqh {X : UU} (is : isdeceq X) (x x' : X) : (x = x') ≃ (eqh is x x'). Proof. intros. apply weqimplimpl. - intro e. induction e. apply isrefleqh. - intro e. unfold eqh in e. unfold booleq in e. induction (is x x') as [ e' | ne' ]. + apply e'. + induction (nopathsfalsetotrue e). - unfold isaprop. unfold isofhlevel. apply (isasetifdeceq X is x x'). - unfold eqh. simpl. unfold isaprop. unfold isofhlevel. apply (isasetbool _ true). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.