Refactor ` Data.Nat.GeneralisedArithmetic`

[jamesmckinna]

Now that we have Algebra.Structures.IsSuccessorSet/Algebra.Bundles.SuccessorSet, should we refactor this module (and others!?) to reflect the action/behaviour/homomorphism properties of the initial SuccessorSet, viz. Nat...? Cf. Algebra.Definitions.RawMonoid.(Sum|Mult|Exp) etc. ...

[JacquesCarette]

Seems very reasonable to me. Although I've got to wonder how much of this is essentially going to be a halfway house to the categorical properties of a NNO?

[jamesmckinna]

Seems very reasonable to me. Although I've got to wonder how much of this is essentially going to be a halfway house to the categorical properties of a NNO?

Indeed. Free/Initial is lurking off-stage, as with so many constructions in the library...?