Definition HLevel_fun {n : nat} (X Y : HLevel n) : HLevel n. Proof. simple refine (_ ,, _). - exact (pr1 X → pr1 Y). - apply impredfun. exact (pr2 Y). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.