Theorem isofhlevelssncoprod (n : nat) (X Y : UU) (isx : isofhlevel (S (S n)) X) (isy : isofhlevel (S (S n)) Y) : isofhlevel (S (S n)) (coprod X Y). Proof. intros. apply isofhlevelfromfun. set (f := coprodf (λ x : X, tt) (λ y : Y, tt)). assert (is1 : isofhlevelf (S (S n)) f) by apply (isofhlevelfcoprodf (S (S n)) _ _ (isofhleveltofun _ X isx) (isofhleveltofun _ Y isy)). assert (is2 : isofhlevel (S (S n)) (coprod unit unit)) by apply (isofhlevelweqb (S (S n)) boolascoprod (isofhlevelssnset n _ (isasetbool))). apply (isofhlevelfgf (S (S n)) _ _ is1 (isofhleveltofun _ _ is2)). Defined.