Corollary isofhlevelfhfiberpr1 (n : nat) {X Y : UU} (f : X -> Y) (y : Y) (is : isofhlevel (S n) Y) : isofhlevelf n (hfiberpr1 f y). Proof. intros. apply isofhlevelfhfiberpr1y. intro y'. apply (is y' y). Defined.