Theorem isofhlevelfssnsumofmaps (n : nat) {X Y Z : UU} (f : X -> Z) (g : Y -> Z) (isf : isofhlevelf (S (S n)) f) (isg : isofhlevelf (S (S n)) g) : isofhlevelf (S (S n)) (sumofmaps f g). Proof. intros. intro z. set (w := weqhfibersofsumofmaps f g z). set (is := isofhlevelssncoprod n _ _ (isf z) (isg z)). apply (isofhlevelweqf _ w is). Defined.