fact: Definition isofhlevelsninclb (n : nat) {X Y : UU} (f : X -> Y) (is : isincl f) : isofhlevel (S n) Y -> isofhlevel (S n) X := isofhlevelXfromfY (S n) f (isofhlevelfsnincl n f is).
imports: UniMath.Foundations.PartA