fact: 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).
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics