Jacques Carette
Jacques Carette
(There's quite a bit of discussion in #2522 that is relevant.) This is a much more general design issue: should we prove things directly or as special cases of more...
One difficulty of using Agda for case studies is that it is hard to disentangle Agda-specific weaknesses from generic good/bad ideas for this kind of design. Furthermore the pros and...
The old category library used to use irrelevance *a lot* and then broke in ways we couldn't fix at some point in Agda's evolution. So I'd be quite concerned that...
This is not `breaking` so could it be v2.4 rather than v3.0?
If it works, seems like a really good idea.
Seems very reasonable to me. Although I've got to wonder how much of this is essentially going to be a halfway house to the categorical properties of a NNO?
It's rather fun to be seeing better design(s) emerge like this.
I definitely prefer documentation to be at top. Things at the end are a kind of 'oh, by the way' -- which works for PLFA, but not so much for...
To allay your fears, might be worth taking `Data.Rational.Properties` (in a new branch based off of this one) and porting it, but without aiming to make that port a PR,...
> So to allay the fears about whether it's too much work to make the change, I may as well (accept having to) do the additional work to make the...