Definition empty_hlevel (n : nat) : isofhlevel (n + 1) ∅. Proof. induction n. - exact isapropempty. - exact (λ x, fromempty x). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.