Experiment with notation for algebra and category theory

[felixwellen]

This is an experiment concerned with the way operators like + or ∘ are overloaded with instance arguments.
Currently, given e.g. A : AbGroup ℓ this is done by

open AbGroupStr ⦃...⦄
instance
  _ = snd A

The idea is to gain better notation with more flexibility and overloading by separating the notation from the data structures (just look at the changes). Here are a couple of things that would be nice to have:

• Use operators with the same name from different structures at the same time, for example _+_ from Semiring and CommRing.
• Choose notation independent of the definition of a structure. For example, a CommMonoid used multiplicative notation in its definition, but one might want to use + in some contexts.
• Have more readable output from agda. Currently, goals are sometimes written as something like AbGroupStr._+_ _ x y instead of x + y. I think that shouldn't happen if _+_ is defined on top level with an instance argument.

It is unclear to me, if this is a good idea performance-wise.