Jacques Carette

I'm also concerned with the UX aspects, so I would definitely experiment before submitting a PR. I wasn't thinking of doing this via meta-programming. We'll see. My feeling is that...

I've always thought of it as monoids being about things with shape `*` and categories about things with shape `* -> *`. They are different because 'composable path' is a...

The CI failure is just for ghc-9.8.4 and seems to be related to ghcup-0.0.9. Seems related to what @andreasabel did with the CI? The exact details are: > Run "$HOME/.ghcup/bin/ghcup"...

> Last last thought: should this be parametrised on `RawSetoid`, or simply on a (pair of) bare relation(s) `_≈_` (as in the `Function.Construct.*` and existing `Relation.Binary.Construct.*` hierarchies)? Ah, the perennial...

Note: I believe that Agda chokes badly if an operator (like `_,_`) has multiple fixities because of overloading. So we really really do have to give them the same fixity....

The desire for progress collides with backwards compatibility, again. #2584 is the right thing to do given the current state. The better thing to do (for v3.0) would be to...

#4489 is now merged, so I guess work on this can re-start?

Since @Xinlu-Y has based 2 PRs on top of this one (indirectly), it becomes important that this gets resolved sooner rather than later.

I agree that moving this documentation to live inside the code is a good idea, with the Wiki retaining pointers to that.

My experience (from long ago as a professional software developer) was that disabling tests seemed to always come back to bite us, because someone re-broke the thing that ways being...