Definition hfp_is_of_hlevel (n : nat) {X Y Z : UU} (HX : isofhlevel n X) (HY : isofhlevel n Y) (HZ : isofhlevel n Z) (f : X → Z) (g : Y → Z) : isofhlevel n (hfp f g).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.