SelfInverse operations on Algebras and their properties

[jamesmckinna]

Reviewing my contribution of Data.Parity and friends, I found myself annoyed about repeated proofs of properties of the self-inverse functions _⁻¹ and corresponding opposite on Data.Sign...
... and was surprised that being SelfInverse didn't seem to be in either the Function or Algebra hierarchies.

Now, with this PR, I've chosen to put these things in the Algebra hierarchy, because that is where Involutive is defined, and self-inverse operations are involutive in the presence of reflexivity (one of the properties I needed/used/defined).

But it seems that I could have put these definitions under Function, and certainly some of the Consequences.Setoid for self-inverse operations are really about their behaviour as Functions... so some advice on where these properties should properly go would be welcome.

An argument I am open to is that, qua functions, they belong under Function; but as operations which are automorphisms of the corresponding Algebra structure, then they belong under Algebra.

It's not obvious to me that we systematically observe such distinctions. One thing that does jump out, cf. issue #1544, is that Algebra.Definitions defines Congruent₁ and Congruent₂, while Function.Definitions defines Congruent, so (t)here's another failure of systematisation: ... I prove that self-inverse operations are Congruent, rather than Congruent₁... but which should I have done?

TODODONE: refactor to use the new definitions/proofs

• Data.Sign.Properties
• Data.Parity.Properties

[jamesmckinna]

PR #1156 (and perhaps an ounce more work) would streamline the (construction and proof of the) iso between Sign and Parity, currently done by hand in Data.Parity.Properties; it might also thereby streamline entirely (?) the treatment of self-inverse operations undertaken in the PR at hand.

[MatthewDaggitt]

Other than that it looks good to me. I have no strong feelings about the Function vs Algebra distinction. I think it's fine here for the moment.