[Agda] Codata oddity

[Nils Anders Danielsson]

On Sat, Jun 7, 2008 at 2:06 AM, Anton Setzer <A.G.Setzer at swansea.ac.uk> wrote:
>
> In my opinion it is important to keep here a clear connection with
> category theory [...]

What you describe seems to be restricted to non-dependent pattern
matching; you have

  case : Conat -> ConatCases

rather than

  case : (n : Conat) -> ConatCases n.

Do you have any ideas about how to beef this up to a more dependent
setting ("coinductive families")? Or are we restricted to "restricted
coinductive families", which I think your current approach allows?

Restricting pattern matching on codata to be non-dependent would solve
the particular problem that I posted before, by the way. Maybe it
would even reestablish type preservation. However, I would prefer a
solution which enables the use of full coinductive families, if this
is possible.

-- 
/NAD