Theorem isofhlevelfpr1 (n : nat) {X : UU} (P : X -> UU) (is : ∏ x : X, isofhlevel n (P x)) : isofhlevelf n (@pr1 X P). Proof. intros. unfold isofhlevelf. intro x. apply (isofhlevelweqf n (ezweqpr1 _ x) (is x)). Defined.