Theorem isofhleveltotal2 (n : nat) {X : UU} (P : X -> UU) (is1 : isofhlevel n X) (is2 : ∏ x : X, isofhlevel n (P x)) : isofhlevel n (total2 P). Proof. intros. apply (isofhlevelXfromfY n (@pr1 _ _)). apply isofhlevelfpr1. assumption. assumption. Defined.