Theorem isofhlevelfsnhfiberpr1 (n : nat) {X Y : UU} (f : X -> Y) (y : Y) (is : isofhlevel (S n) (y = y)) : isofhlevelf (S n) (hfiberpr1 f y). Proof. intros. unfold isofhlevelf. intro x. apply (isofhlevelweqf (S n) ( ezweq1g f y x)). apply isofhlevelsn. intro X1. induction X1. assumption. Defined.