[Agda] Tentative guidelines for working with coinductive types

[Noam Zeilberger]

On Wed, Jan 14, 2009 at 04:11:34PM -0500, Dan Doel wrote:
> The thing is, equality on coinductive types is extensional.

Sorry, I meant to copy the notation from Nils' email but accidentally
flipped it.  By _≡_ I meant an appropriately defined extensional
notion of equality, what you/Nils write as _≈_.

So to clarify, let's say you define an even simpler coinductive
type, like the CoNats:

  data CoNat : Set where
   zz : CoNat
   ss : ∞ CoNat -> CoNat

and have a good notion of equality on this type:

  data _≈_ : CoNat -> CoNat -> Set where
   zeq : zz ≈ zz
   seq : ∀ {x y} -> ∞ (♭ x ≈ ♭ y) -> ss x ≈ ss y

now I define a specific CoNat for "infinity":

  inf : CoNat
  inf = ss inf'
    where inf' ~ ♯ inf

I want to prove that inf ≈ inf.  How can I do that?  The obvious
thing is to mirror the structure of inf:

  infeq : inf ≈ inf
  infeq = seq infeq'
    where infeq' ~ ♯ infeq

but this doesn't typecheck, because "(ss .T._.inf') != (♭ (♯ inf))
of type CoNat".

Noam