[Agda] Coinductive indices

[Robert J. Simmons]

I have a hopefully-simple question about coinduction. I have streams
of numbers under some constraint, they can be either labeled with
their cosize or not, and I want to show that I can take a stream and
turn it into a labeled stream.

open import Data.Nat renaming (ℕ to Nat)
open import Data.Conat renaming (Coℕ to Conat)
open import Coinduction

module Example where

data SmallStream (n : Nat) : Set where
   nil : SmallStream n
   cons : ∀{m}
      (N : m ≤ n)
      (S : ∞ (SmallStream n))
      → SmallStream n

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))

size : ∀{n} → SmallStream n → Conat
size nil = zero
size (cons N S) = suc (♯ size (♭ S))

mark : ∀{n} (S : SmallStream n) → SmallStream' n (size S)
mark nil = nil
mark (cons N S) = {!!}

I'm not clear on whether this is possible, partially due to the issues
raised in Conor's "generative thunk" thread from a while back.

I tried a number of avenues, including making the index of
SmallStream' a ∞ Conat instead of a Conat, which almost, but not
quite, worked. The real reason I'm interested in this is that the size
of a list or a colist is invariant under "weakening" (turning a
SmallStream 4 into a SmallStream 9). In the strictly-inductive
setting, my experience is that this sort of size is very useful as a
termination metric.

 - Rob

-- 
Robert J. Simmons
simrob.com
gps.simrob.com
rjsimmon at cs.cmu.edu
robsimmons at gmail.com
Cell: 404-273-6890