[Agda] Coinductive indices

[Dan Doel]

On Tuesday 15 March 2011 4:14:34 PM Robert J. Simmons wrote:
> data SmallStream' (n : Nat) : Conat → Set where
>    nil : SmallStream' n zero
>    cons : ∀{m size}
>       (N : m ≤ n)
>       (S : ∞ (SmallStream' n size))
>       → SmallStream' n (suc (♯ size))

Your definition here is not recommended. Instead, I'd write:

  data SmallStream' (n : Nat) : Conat -> Set where
    nil : SmallStream' n zero
    cons : forall {m size}
       (N : m ≤ n)
       (S : ∞ (SmallStream' n (♭ size)))
       -> SmallStream' n (suc size)

The rule being: quantify over an ∞ I, i, make the coinductive reference 
indexed by ♭ i, and make the result type indexed by con i. I being the index 
type of course, and con a constructor.

With this definition, I think you should find it's straight forward to 
implement mark.

-- Dan