[Agda] Sized types and coinduction

[Brandon Moore]

I'm not sure how well supported sized types are supposed to be,but I don't see how to use them with coinductive definitions.

I'm trying to follow the slides from a 2008 AIM meeting.

Is there supposed to be an ^ for sizes which is different from ↑?


{-# OPTIONS --sized-types #-}
module size where
open import Size
open import Coinduction renaming (∞ to ∞c)
open import Data.Nat

data Stream : (i : Size) → Set where
  _∷_ : ∀{i} → ℕ → ∞c (Stream i) → Stream (↑ i)

mapStream : ∀{i} → (f : ℕ → ℕ) → Stream i → Stream i
mapStream f (y ∷ y') = f y ∷ ♯ mapStream f (♭ y')

nats : Stream ∞
nats = 0 ∷ ♯ mapStream {∞} suc nats

nats' : ∀ {i} → Stream i
nats' {i} = {!!}
-- can't refine with _∷_, as that only produces values in Stream (↑ i)