Jacques Carette

I emphatically agree with removing `sum` and `product` from `Data.List.Base`. That was a grave mistake that is relatively harmless in Haskell-like languages and deadly in Agda-like languages.

> And how about @Taneb 's question on https://github.com/agda/agda-stdlib/pull/2558 regarding and/or and all/any? Etc. Ditto: this don't belong in `Data.List.Base`. Same wart, just that downstream effects are not as dire.

Yeah, these definitely are bugs. This needs a proper design.

> I wonder if perhaps we should make every module preamble comment include the new (infix/mixfix) symbols introduced with their character encodings (emacs and Unicode?), as 'self-documentation', rather than trying...

So maybe we should hold off on this, so that the new symbol(s) can be used?

I think emacs overrides this - I've never had issues with `C-space` on Aquamacs. So it might be only `VSCode` that has this issue.

For others: the names are taken from the combinators in `agda-categories`. Those were inherited from older versions of that library. I do *not* like them! So please do suggest better...

The 'new' names in `Assoc4` are better. The rest are hideous and make things quite unreadable. It was a nice experiment... which I would call a clear failure. I most...

As I've indicated, I'm not a big fan of push/pull because they are not very mnemomic; the superscripts don't help either. Indeed, if one looks at ```agda module Pulls (x∙y≈z...

My firefox displays them all just fine! I would be fine with a name that involves `refocus` instead of symbology. We could use superscripts for indicating left/right refocusing. The one...