proposition: Lemma isofhlevel_HLevel (n : nat) : isofhlevel (S n) (HLevel n).
proof: 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.
imports: UniMath.Foundations.Propositions UniMath.Foundations.UnivalenceAxiom