Jacques Carette

I want to do some proper benchmarking to see the effect of using `--cubical-compatible`. It depends on where the new code gets automatically added. If it's mostly for `data`, then...

Agreed. I'd welcome a PR that documented that. [I just know I might not get the time to do this for a couple of weeks.]

Being a 'SolutionSet' is not, in an of itself, very interesting. It is much more interesting as a notion relative to a particular Adjoint Functor 'problem'. The above trivial solution...

So, does this mean that the proof has a problem? Should Agda accept it? Pinging @HuStmpHrrr who did the original.

`git blame` on `Relation.Binary.Bundles` tells me the first appearance of such a `module Eq` dates from September 2019 by @MatthewDaggitt back when the file was `Relation.Binary.Packages` in commit 7e00c92194.

Teaching with PLFA right now, have updated to agda-2.7 and stdlib-2.2, and some things have gotten worse. I've got some issues to bring up when I have the time. One...

> Are these issues to do with this PR, or general comments deserving a separate issue for v2.1/v2.2, The example is of the latter kind. But the reason I'm hesitating...

@wenkokke wrote: > Could you submit this as a separate issue, so that we can discuss these issues in detail? planning to! I've been swamped, so this is still in...

@jamesmckinna @gallais and I have verified that the changes asked for have been done. So we're over-riding the blocked merge from @MatthewDaggitt .

- Re `IsStronglyFinite`: we actually gain quite a lot of type inference by making it a 1-constructor `data` (less sure about 1-field `record` ?). The extra indirection makes operating over...