Theorem isofhlevelfhomot (n : nat) {X Y : UU} (f f' : X -> Y) (h : ∏ x : X, paths (f x) (f' x)) : isofhlevelf n f -> isofhlevelf n f'. Proof. intros X0. unfold isofhlevelf. intro y. apply (isofhlevelweqf n (weqhfibershomot f f' h y) (X0 y)). Defined.