consistency in use of subscripts on names

[jamesmckinna]

https://github.com/agda/agda-stdlib/pull/2922/changes#r2846379598 exposes a seeming clash/cognitive dissonance between the use of subscripts on names, there Homomorphic, to denote

• the arity of an operation/property describing it, so Homomorphic₂ describing a property of a binary operation
• the number of salient arguments to a property, there Homomorphic₂ describing a property of a unary function concerning two relations (on the source and target of the function!)

We should try very hard to avoid this kind of confusion!

Proposal: arity should determine the subscript, if any (consistent also with our use of ₙ in Relation.Nary...)