Description
Previously, on #2264 I raised the following discussion point:
we currently have the following choices for an Algebra with a distinguished point (0#? or ‵zero, because it's a 'quoted' version of Agda.Builtin.Nat.zero?)) and unary operation (suc#, or _+1#, or ‵suc because it's a 'quoted' version of Agda.Builtin.Nat.suc?):
PointedUnary? ... the universal algebra way;NNO/NaturalNumber(s)Object? ... the Lawvere/categorical way;SuccessorSet? ... the Dedekind way
Can we agree on 'sensible' choices from this palette?
Originally posted by @jamesmckinna in #2264 (comment)
So this issue to is to offer the following specimen design/implementation, for discussion (and is tantamount to a fully articulated PR, moreover purely mechanically derivable by analogy with all the others). I'd be happy to change any of the names, in the spirit of the above original comment. Against @JacquesCarette I'd hold out for NNO, but
I'll go for SuccessorSet as a reasonable, if still verbose, first choice...
(deleted: previous content, invalid thanks to my stupidity...)