[Agda] how to type this?

[Nils Anders Danielsson]

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 = ?

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.