[Agda] how to type this?

[Martin Escardo]

Dear Agda fans (and type theorists),

I want to consider functions f that take infinite sequences x_0, x_1, 
x2_, .... to values in a result type R. So, at first sight, we have 
something like

      f : prod_i X_i -> R.

But I want the type X_i to depend on the elements x_0, ... x_(i-1) in 
addition to i. That is, x_i is to have type (X_i x_0 ... x_(i-1)).

If the sequence x_i were finite, I know how to do that.

How can this be expressed in Agda (or in type theory) in the infinite 
case in a simple and mathematically elegant way? (I prefer to avoid 
co-induction if possible.)

Thanks!

MHE.