Theorem isofhlevelfhfiberpr1y (n : nat) {X Y : UU} (f : X -> Y) (y : Y) (is : ∏ y' : Y, isofhlevel n (y' = y)) : isofhlevelf n (hfiberpr1 f y). Proof. intros. unfold isofhlevelf. intro x. apply (isofhlevelweqf n (ezweq1g f y x) (is (f x))). Defined.