[ new ] notions of finiteness

[Saransh-cpp]

A subset of #2017 containing minimal changes related to finiteness

[laMudri]

This PR on its own fails the “definitions should come with proofs” test, but maybe it's permissible with the promise of proofs in a later PR. We'll have to let the maintainers decide.

[Saransh-cpp]

Yes, that is very true. I just don't how to include the proofs without bringing in a lot more changes (which should be in separate PRs according to the discussions in #2017).

[jamesmckinna]

(Overlooked in yesterday's meeting)
Suggest at the very least that we bump this to v2.2, or even close (cf. #2005 ) until/unless someone comes along able to pick up the slack?

[JacquesCarette]

I put it in v2.2 as I really would like to push this through.

[jamesmckinna]

@JacquesCarette I can just about take Apex as the name of the 'covering object' A in an epic situation A → X (L52-L54 below), but it seems less defensible here in the dual situation X → A. Is it 'standard' terminology? Or is there something better from eg the categorical literature?

[JacquesCarette]

Yes, this is probably too influenced by other code / ideas, and no longer really fits here. Suggestions?

[jamesmckinna]

I hunted around, and unfortunately the literature uses 'generic' names such as X, Y/A, B when discussing things as morphisms. For embedding/extension, the domain of an injection is sometimes called I, and of a projection as P, but these don't seem quite satisfactory, either?

In each case, though, the relevant object is (suitably) enumerable, so could it be called Enum, or even Enumeration?... Or even simply E?

[JacquesCarette]

Enumeration > Enum > E.

[jamesmckinna]

OK!?

[jamesmckinna]

I put it in v2.2 as I really would like to push this through.

Comments on notation. I'd like to see this too, but as a fresh addition, we should try to get a 'convenient'/usable/memorable syntax/naming convention fixed before committing...

[MatthewDaggitt]

I've converted this to a draft. @JacquesCarette when it's ready to review properly, turn it back again 👍

[JacquesCarette]

We've decided to close this for now, in favour of the "project issue #2511 " as it's a bigger deal.