[Agda] how to type this?

[Martin Escardo]

Anton Setzer wrote:
> The following uses codata but seems to me a possible solution:

Thanks. It does seem to capture what I had in mind.

Martin