Data.Parity and the 2+_ pattern

[jamesmckinna]

@Taneb 's recent work (#1744 , #1744) on permutations-as-transposition-lists has drawn attention to the (possible) need for a Parity type (rather than proxying via Data.Sign), together with various properties: so far I have a branch with
UPDATED:

• Parity admits a commutative semiring structure (with 0 = 0ℙ; 1 = 1ℙ etc.)
• a function parity from Nat to Parity in Data.Nat.Base
• a function toSign from Parity to Sign
• a function fromSign from Sign to Parity
• proofs that (toSign, fromSign) form an abelian group iso from (Parity, 0, _+_) to (Sign, +, _*_)
• miscellaneous tidyings up of Data.Sign etc. to reflect new names for algebraic structures/bundles, cf. issue Data.Integer.Properties.+-isAbelianGroup should be called +-0-isAbelianGroup #1844 and in line with review comments on current PR
• CHANGELOG

TODO in a subsequent PR:

• proof that parity is a commutative semiring homomorphism from Nat to Parity
• rationalise that proof; and in particular resolve where it belongs

Additionally, this might have the following as knock-on effects:

• rationalise the many instances in the library where the 0, 1, 2+ n pattern analysis of a Nat argument takes place (esp. wrt N{-}ary operations, as well as the obvious Binary and Nat examples) see this branch and PR rationalise use of suc (suc n) and suc n@(suc _) patterns throughout; remove 2+ _ pattern #1870

EDITED:
It raised a question in my mind as well regarding where homomorphism-like properties belong in the library: under the source type, in *.Properties, or somewhere else? I currently have Parity import Sign in order to define the operations, but it strikes me that there's an asymmetry to that decision, which might better be reflected in having subdirectories of the Algebra.* hierarchy which record concrete instances of (Semi)RingHomomorphisms etc. suggestions welcome! moved discussion to issue #1871