Theorem isofhlevelfcoprodf (n : nat) {X Y Z T : UU} (f : X -> Z) (g : Y -> T) (is1 : isofhlevelf n f) (is2 : isofhlevelf n g) : isofhlevelf n (coprodf f g). Proof. intros. unfold isofhlevelf. intro y. induction y as [ z | t ]. apply (isofhlevelweqf n (weqhfibercoprodf1 f g z)). apply (is1 z). apply (isofhlevelweqf n (weqhfibercoprodf2 f g t)). apply (is2 t). Defined.