Make _⋆_, _∘_ right associative in Category

[barrettj12]

So that we can write

f ⋆ g ⋆ h

and Agda will know how to parse it.

It's as easy as putting

  infixr 9 _⋆_
  infixr 9 _∘_

at the end of the definition of Category.

We could also think about doing this for other associative algebraic structures (semigroups, groups, rings, ...)

[felixwellen]

We already use infixr for + in AbGroup. And we use infixl for a whole lot of operations in algebraic structures. I haven't thought about which one might be better...

And I can't see a reason why we shouldn't use this for categories.

[barrettj12]

Considering we have associativity, I don't think it matters too much whether we choose infixl or infixr. I just copied the infixr 9 _∘_ declaration from Cubical.Foundations.Function. Right associativity seems to be conventional.