Jacques Carette
Jacques Carette
Good stuff! Also: all my comments are already preemptively raised in the PR description. Opinions: 1. I think `Function` is a horrible place for the definition of Galois connection. The...
To see if I understand: in the situation above, cubically-many "potential" `l`s are created? Do they then all collapse to a single (unsolved) one, but still take up time and...
In case anyone things this is just due to "ridiculously unbundled" situations like in the original report, I'm pretty sure I can find similar occurrences in agda-categories where quite long...
Actually, I'm totally fine with a "fat" `Data.X`, as long as I can get a thin `Data.X.Base`, and a thin way to get as some relations as well. As long...
The `Data.X.Base` files seem to be good in general. The problem is that there are currently some useful relations defined in `Data.X` that come from giant `Data.X.Properties` files. I would...
I certainly wouldn't look at it as "lost the battle"... just bowed to the inevitable! 😆 [I forget the convention between `.Core` and `.Base`, I'll need to relearn it...] Inside...
My instincts for naming (in Agda) goes in the opposite direction for 1 vs 2. The standard library is quite a mixed bag in this respect, but for simpler types...
I agree, `foldrₙₑ` does look rather ugly, I withdraw it as a contender. The rest was really 'my feeling'. Hopefully people with more experience will chyme in.
I'm with @gallais on the naming. Though I don't feel too strongly about it.
No strong opinion on the placement of the `1`.