[Agda] recursive \times

[Serge D. Mechveliani]

Please, why the program below is not type-checked?

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

  f : (ns : List Nat) -> EachPositive ns -> Nat
  f _ _ = 0  

-- a contrived example:  f takes  ns  and needs to use a proof for n > 0  
for each  n  in  ns. 

If I comment out  f,  then  EachPositive  is compiled
(despite that I expected   "List (Set _)"  to be wrong).

What should be the intended signature for  f  ?

I attach to this letter     t.agda.zip 

-- the variant with  ManyProduct  -- with applies \times  recursively.

1) Has Standard library something close to  ManyProduct ?
2) Can the attempt with  map (\ n -> n > 0)  be improved, or it is just a 
   basically wrong idea?

Thank you in advance for explanation,

------
Sergei
-------------- next part --------------
A non-text attachment was scrubbed...
Name: t.agda.zip
Type: application/zip
Size: 543 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130412/c682fa17/t.agda.zip