Jacques Carette

Oh, as far as 'right' is concerned, I am quite convinced that the only way to do what we want would be for Agda to have features for representing theories...

I think things are fundamentally in the realm of meta-programming, one way or another. Either we take some internal representation (`Data.Record` or something like it) and *export* it to actual...

I think it also applied to `ChunkDB`. i.e. we should document "here is the information that I need" (via lenses / getters) instead of specifying an exact data type.

We don't need lenses because we don't really ever 'set'. So for most things, only `Getter` is enough. In general, any function that 'reads' information should be polymorphic. So reading...

In theory, `stdlib` is `--cubical-compatible` (because, well, it uses that flag most everywhere!). If in practice it's not, that would be good to know, as `--without-K` is more performant than...

Agreed. I guess 'named arguments' make this strongly a v3.0 issue. Sigh.

`EmptyS` is definitely a bad "code smell" that should be closely examined. Using them to fill a field is a user mistake. So `mkQuantDef` and `mkQuantDef'` are very suspicious. As...

For your examination of `mcShrStrngthQD`, I would run the same exercise in reverse. Take all the information that feeds into it, and make a 2-column table: - `information` -- `what...

First guess: you're getting bit because the way you've set things up, Agda will inline everything, creating enormous terms with ridiculous amounts of duplication. `where` and co-patterns are your friends,...

As far as I understand from the above discussion @jamesmckinna , it's still not clear what the real source of the slowdown is. Clearly it's related to `eta-equality` but, beyond...