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