[Agda] list of types

[Serge D. Mechveliani]

Andreas Abel responded recently

> A list of types is not a type.

But why       
       EachPositive : List Nat -> List (Set _)
       EachPositive xs =  map (\ n -> n > 0) xs

is type-checked?
(Agda-2.3.2 MAlonzo).

Regards,

------
Sergei