Lemma isrefleqh {X : UU} (is : isdeceq X) : isrefl (eqh is). Proof. intros. unfold eqh. unfold booleq. intro x. induction (is x x) as [ e | ne ]. - simpl. apply idpath. - induction (ne (idpath x)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.