search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
582 stars 236 forks source link

Refactor ` Data.Nat.GeneralisedArithmetic` #2446

Open jamesmckinna opened 3 months ago

jamesmckinna commented 3 months ago

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 commented 3 months ago

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 commented 3 months ago

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...?