Conor McBride

Looks like DOT might do a lot of the work for us, if it's sufficiently controllable. The above example is a good start, but I worry about that in-arrow from...

Copatterns make Agda simpler! The notation should be extended! The assumption that we only ever do a bunch of left stuff then a bunch of right stuff has been problematic...

It will not surprise you at all that I think people coming from Haskell should not be overly indulged. I think our entire community has suffered from Haskell drag, making...

Let's start with data types. They're generative, and they don't have first class descriptions: you can't compute a data type, e.g., by differentiating another one. Worse, we lose the power...

We didn't have coinduction in Epigram 1, but we were certainly on that case in Epigram 2. We did not get as far as mixing Mu and Nu. (Co-)datatypes in...

There are several things worth doing here, many of which I'm too busy for, so have some free ideas on me. As I said, I'd like to look at localising...