Theorem isofhlevelfsn (n : nat) {X Y : UU} (f : X -> Y) : (∏ x x' : X, isofhlevelf n (@maponpaths _ _ f x x')) -> isofhlevelf (S n) f. Proof. intros X0. unfold isofhlevelf. intro y. simpl. intros x x'. induction x as [ x e ]. induction x' as [ x' e' ]. induction e'. set (xe' := make_hfiber f x' (idpath _)). set (xe := make_hfiber f x e). set (d3 := d2g f x xe'). simpl in d3. assert (is1 : isofhlevelf n (d2g f x xe')). assert (h : ∏ ee : x' = x, paths (maponpaths f (pathsinv0 ee)) (d2g f x xe' ee)). { intro. unfold d2g. simpl. apply (pathsinv0 (pathscomp0rid _)). } assert (is2 : isofhlevelf n (λ ee: x' = x, maponpaths f (pathsinv0 ee))) by apply (isofhlevelfgtogw n ( make_weq _ (isweqpathsinv0 _ _)) (@maponpaths _ _ f x x') (X0 x x')). apply (isofhlevelfhomot n _ _ h is2). apply (isofhlevelweqb n (ezweq3g f x xe' e) (is1 e)). Defined.