[Agda] Interactive programs in Agda

[Peter Hancock]

By the way, thanks very much for the library and slides.

>
> and is linked from
> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Libraries
>
Looking at the slides for your AIM talk linked from here,
I think you define

    IO C R A to be  nu X.  A + (C <| R) X

to use container notation.   This is monadic in A, but I think the
proof is a little tricky.

You give on slide 8 a "definition" of >>= which would work
fine if the IO C R A were mu X. A + (C <| R) X.
Can the definition really be justified from the universal property of
final coalgebras?

I wonder if people in the future will say "It was 2009 when
Anton Setzer dragged a window across his monitor using a
his mouse and a constructive proof". The importance of this
moment in history may overshadow the invention of the wheel.

Peter