[Agda] Forall and product

[N. Raghavendra]

Hi,

I am looking at this definition of uncurry in Data.Product:

--8<---------------cut here---------------start------------->8---
uncurry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
          ((x : A) → (y : B x) → C (x , y)) →
          ((p : Σ A B) → C p)
uncurry f (x , y) = f x y
--8<---------------cut here---------------end--------------->8---

As I understand, it says that if we have a set A, a function B from A to
Set, and a function C from the disjoint union M:=(\coprod_{a:A} B(a)) to
Set, then uncurry is the map from \prod_{a:A}(\prod_{b:B(a)} C(a,b)) to
\prod_{p:M}(C(p)) which is defined by

uncurry f p = f (proj1 p) (proj2 p)

Now I thought that the product of a family of sets (S_i)_{i\in I}
corresponds to the type (\forall {i} -> S i).  So in the definition of
uncurry, I replaced

((x : A) → (y : B x) → C (x , y)) with

(\forall {x} -> \forall {y} -> C (x , y))

But then I got an error like ".C (_x_47 f x y , _y_48 f x y) should be a
function type, but it isn't".  What's the explanation?

Thanks,
Raghu.

-- 
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/