Lemma isofhlevel_HLevel (n : nat) : isofhlevel (S n) (HLevel n). Proof. cbn. intros X X'. induction X as [X p]. induction X' as [X' p']. set (H := isofhlevelweqb n (Id_p_weq_Id (λ X, (isofhlevel n X,, isapropisofhlevel _ _)) X X' p p')). cbn in H. apply H. apply isofhlevelpathspace; assumption. Defined.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.UnivalenceAxiom.