Theorem isofhlevelfssn (n : nat) {X Y : UU} (f : X -> Y) : (∏ x : X, isofhlevelf (S n) (@maponpaths _ _ f x x)) -> isofhlevelf (S (S n)) f. Proof. intros X0. unfold isofhlevelf. intro y. assert (∏ xe0 : hfiber f y, isofhlevel (S n) (xe0 = xe0)). { intro. induction xe0 as [ x e ]. induction e. set (e':= idpath (f x)). set (xe':= make_hfiber f x e'). set (xe:= make_hfiber f x e'). set (d3:= d2g f x xe'). simpl in d3. assert (is1: isofhlevelf (S 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 (S n) (fun ee : x = x => maponpaths f (pathsinv0 ee))) by apply (isofhlevelfgtogw (S n) (make_weq _ (isweqpathsinv0 _ _)) (@maponpaths _ _ f x x) (X0 x)). apply (isofhlevelfhomot (S n) _ _ h is2). } apply (isofhlevelweqb (S n) (ezweq3g f x xe' e') (is1 e')). } apply (isofhlevelssn). assumption. Defined.