Add Number literals for any SuccessorSet

[jamesmckinna]

Fixes #1363

NB:

• naming/hierarchy: adds Algebra.Literals rather than Algebra.Structures.Literals
• fixes spurious over re-export in Algebra.Bundles.SuccessorSet
• in-place implementation of fromℕ, rather than defining that as the unique morphism from Algebra.Construct.Initial.SuccessorSet UPDATED: made the definition local, to future-proof the API
• TODO (downstream?): as with [fixes #2273] Add SuccessorSet and associated boilerplate #2277 adds no new {Is}SuccessorSet structures/bundles to existing Algebra.* nor Data.* in order to be able to create Number instances; cf. discussion on the issue as to where/how to create the 'right' ones so that they are consistently implemented across the whole *Ring* hierarchy in such a way as to have the 'right' properties...

Issue:

• should the module parameter be supplied as an instance? as a RawSuccessorSet?

Could be v2.1 or v2.2?

[JacquesCarette]

Tiny tweak and a question.

[jamesmckinna]

A potential problem (but not, perhaps, in practice?): the Number implementations defined

• in Data.Nat.Literals for Agda.Builtin.Nat.Nat, and
• (hypothetically at this stage) in Data.Nat.Properties for Data.Nat.Base.ℕ via isSuccessorSet

will be distinct: the second, in particular, will be (needlessly) more strict in its implementation of fromNat, than the first.

Is this a genuine problem? If so, what's the 'best' way to finesse this, except via separate, 'hand-cut' implementations of Number on a case-by-case basis?

[JacquesCarette]

I do wonder if this is a genuine problem, at least in the context of Agda. [It might be!] It feels like a conundrum that is more philosophical: is stdlib trying to support prove-first-program-second Agda, or something else? There's a different library for program-first-prove-sometimes for Agda.

Of course, the most interesting would be prove-AND-program, with a purposefully symmetric operator in there. Agda sure doesn't feel ready for that.

[jamesmckinna]

I do wonder if this is a genuine problem, at least in the context of Agda. [It might be!] It feels like a conundrum that is more philosophical: is stdlib trying to support prove-first-program-second Agda, or something else? There's a different library for program-first-prove-sometimes for Agda.

Of course, the most interesting would be prove-AND-program, with a purposefully symmetric operator in there. Agda sure doesn't feel ready for that.

Returning to this comment, I wondered a lot about the first part: stdlib can often feel, in its structural organisation, that it is program-first (via Data.X.Base), and then prove afterwards (via Data.X.Properties). Or am I missing something?

The second part, I don't really understand at all: how would we get a symmetric operator out of fromNat? (Or was this comment intended for another thread elsewhere?)

[JacquesCarette]

Returning to this comment, I wondered a lot about the first part: stdlib can often feel, in its structural organisation, that it is program-first (via Data.X.Base), and then prove afterwards (via Data.X.Properties). Or am I missing something?

You are quite right that, structurally, stdlib feels program-first. But it is proof-first in its actual details, for the most part, i.e. the definitions in Data.X.Base are usually the ones that make proofs easy.

Of course, the most interesting would be prove-AND-program, with a purposefully symmetric operator in there. Agda sure doesn't feel ready for that.

The second part, I don't really understand at all: how would we get a symmetric operator out of fromNat?

My bad, what I wrote was not clear: I mean that 'AND' to be at the meta-level, to be a symmetric operation on 'prove' and 'program' as concepts!

[jamesmckinna]

Back to the philosophical question: of course it makes no difference for Nat: because data.Nat.Instances doesn't need to change its definition of literals via Number?

Accordingly, I suggest either merging this now, or else putting to draft while I add all the IsSuccessorSet implementations throughout the library: but maybe that's better as a downstream PR? Thoughts welcome!

[JacquesCarette]

Merging this now probably makes sense, but I'd want a concurring opinion - perhaps @gallais who has already looked at it?