Theorem isofhlevelfsumofmapsnoi (n : nat) {X Y Z : UU} (f : X -> Z) (g : Y -> Z) (isf : isofhlevelf n f) (isg : isofhlevelf n g) (noi : ∏ (x : X) (y : Y), neg (paths (f x) (g y))) : isofhlevelf n (sumofmaps f g). Proof. intros. intro z. induction n as [ | n ]. - set (zinx := invweq (make_weq _ isf) z). set (ziny := invweq (make_weq _ isg) z). assert (ex : (f zinx) = z) by apply (homotweqinvweq (make_weq _ isf) z). assert (ey : (g ziny) = z) by apply (homotweqinvweq (make_weq _ isg) z). induction ((noi zinx ziny) (pathscomp0 ex (pathsinv0 ey))). - apply isofhlevelsn. intro hfgz. induction ((invweq (weqhfibersofsumofmaps f g z) hfgz)) as [ xe | ye ]. + apply (isofhlevelweqb _ (weqhfibernoi1 f g noi z xe) (isf z)). + apply (isofhlevelweqb _ (weqhfibernoi2 f g noi z ye) (isg z)). Defined.