[Agda] how to type this?

[Martin Escardo]

Thanks. This looks good. However, I don't want to supply X. I'd rather 
have it as a parameter, and in that case the mutually recursive 
definition cannot be performed (right?).

Let me tell you a bit more about the problem for the sake of intuition. 
We have a game with omega-many moves. Then f : prod_i X_i -> R plays the 
role of assigning outcomes to plays (such as "win" or "lose", or how 
much you win, or a vector saying how much each player wins). The 
condition of my message says that the allowed moves at any stage depend 
on the actual moves at the previous stages.

The theorems I want to write down in Agda should apply to any given such 
game (specified by X_i, R, and f, among other data), whereas your 
definition, as it currently stands, would force me (by filling the gaps) 
to consider particular games each time.

Thanks again.
Martin

Nils Anders Danielsson wrote:
> On 2009-10-02 12:46, Martin Escardo wrote:
>> 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)).
> 
> Would the following code (which uses both coinduction and
> induction-recursion…) be of any help for you? You have to fill in the
> question marks yourself.
> 
>  module ME where
> 
>  open import Coinduction
>  open import Data.Nat
> 
>  mutual
> 
>    data Telescope : ℕ → Set where
>      ε   : Telescope zero
>      _▻_ : ∀ {i} (x : Telescope i) → X x → Telescope (suc i)
> 
>    X : ∀ {i} → Telescope i → Set
>    X = ?
> 
>  data Input : ∀ {i} → Telescope i → Set where
>    _▻_ : ∀ {i} {t : Telescope i}
>          (x : X t) → ∞ (Input (t ▻ x)) → Input t
> 
>  f : Input ε → ?
>  f = ?
>