Definition hfp_HLevel (n : nat) {X Y Z : HLevel n} (f : pr1 X → pr1 Z) (g : pr1 Y → pr1 Z) : HLevel n. Proof. simple refine (hfp f g ,, _). apply hfp_is_of_hlevel. - exact (pr2 X). - exact (pr2 Y). - exact (pr2 Z). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.