Jacques Carette
Jacques Carette
If you mean in the sense of [weak 2-monad](https://ncatlab.org/nlab/show/2-monad), then yes, that would be useful. I specify weak because we've found that strictness of various kinds seems to not work...
I would not be surprised if there were another issue also compounding this: loss of sharing. We use Agda's modules a lot, and they are notorious for causing loss of...
This was also discussed in the agda-categories Slack. [Though I think we should, like for Agda itself, move to Zulip.]
Wow. I'm pretty sure that Cartesian is partially at fault here. There are some pretty significant blowups in the sizes of .agdai files too (which I worked on reducing some...
As far as I know (from comments that both @UlfNorell and @WolframKahl made), 1) module parameters are instantiated by copying, and 2) private modules are also done by copying, with...
Weird progress: by taking the `pentagon` proof out of being defined inside the record, but instead to a private variable outside of it, this cuts the resulting Haskell file from...
Even more progress: by changing the `Cartesian` module to not create a module with all the `BinaryProducts` stuff and then exporting it publicly as well, this goes from 5M to...
The "winners" in the insanely large compiled files (as documented in the 2nd issue on the agda issues) are now: ``` MacBook-Air-2:Code carette$ find . -xdev -type f -size +10M...
@maxsnew can you give this another look?
No worries. My life is quite eventful in all of July, this may end up waiting until early August. Though I will try next week, we'll see.