Theorem isofhlevelfonpaths (n : nat) {X Y : UU} (f : X -> Y) (x x' : X) : isofhlevelf (S n) f -> isofhlevelf n (@maponpaths _ _ f x x'). Proof. intros X0. set (y := f x'). set (xe' := make_hfiber f x' (idpath _)). assert (is1 : isofhlevelf n (d2g f x xe')). { unfold isofhlevelf. intro y0. apply (isofhlevelweqf n (ezweq3g f x xe' y0) (X0 y (make_hfiber f x y0) xe')). } assert (h : ∏ ee : x' = x, paths (d2g f x xe' ee) (maponpaths f (pathsinv0 ee))). { intro. assert (e0: paths (pathscomp0 (maponpaths f (pathsinv0 ee)) (idpath _)) (maponpaths f (pathsinv0 ee))) by (induction ee; simpl; apply idpath). apply (e0). } apply (isofhlevelfhomot2 n _ _ (make_weq (@pathsinv0 _ x' x) (isweqpathsinv0 _ _)) h is1). Defined.