Jacques Carette

This is where we want to loop in people like @jespercockx - who I guess must have been at that talk.

I would sure welcome such a rewrite. We should "use the structure of the math" more. And I guess the first 2 renames are not needed at all?

Can you please write out the pattern? I don't know what parts of that file is "the pattern" and what is just code.

This is yet another form of the eternal bundled / unbundled question. The correct answer is: don't choose, they are equivalent. Pragmatically, that remains a non-answer because, in Agda, this...

Well look at that, a `hypothetical-rewrite` milestone - very nice. Hmm, I'd be tempted to start a page on the Wiki also collecting language changes that we library writers would...

> One argument against punting this [...] Amusingly, I find this all too abstract to figure out whether I agree with you or not. Could you give a very concrete...

- No, as `Cancellative` have a different shape and `cancel-left`: `x * y = e -> x * (y * z) = z` for `e` a unit. It is a...

I agree that `-‿inverse` feels like overkill and that `+-inverse` would be more appropriate. I also agree that doing the obvious conservative extension of defining subtraction is worthwhile. People can...

The relationship is non-trivial because [IsGroupoid](https://agda.github.io/agda-categories/Categories.Category.Groupoid.html) is mostly about `sym` since the 'rest' is in `Category` already. And there's the issue that `IsEquivalence` does not talk about equivalences-of-equivalences but E-Groupoids...

When I find myself wanting to use "too many" levels of nested modules, I try to use that as a signal to sit back and think some more. It's a...