Theorem isofhlevelsnsummand2 (n : nat) (X Y : UU) : isofhlevel (S n) (coprod X Y) -> isofhlevel (S n) Y. Proof. intros is. apply (isofhlevelXfromfY (S n) (@ii2 X Y) (isofhlevelfsnincl n _ (isinclii2 _ _)) is). Defined.