Rijke Finite Types and the Number of Finite Groups

[kangxyz]

This PR transports Egbert Rijke's main results in OEIS-A000001 to cubical agda. Especially his definition of "homotopy finite type" and they are closed under forming Σ-types (see Cubical.Data.FinType, the condition is named as isFinType).

Tons of facts about finite sets and related stuff are needed. So this PR depends on #630.

Now we can count the number of finite sets with structures like finite groups or finite semi-groups, at least in theory... I have defined a few in Cubical.Experiments.CountingFiniteStructure and everyone can add what he/she likes. But except for the trivial structure (basically no structure, so the number is always 1), the counting is hard to perform.

I tried to calculate the number of finite semi-groups of cardinal 2, and after several hours, agda told me "Sorry, Heap Overflow!" Maybe I should enlarge the heap size and try again, or anyone with a better computer would take this job. It seems possible to compute the number though may cost a rather long time.

It also contains the definition of OEIS-A000001. Since the difficulty is much more serious than semi-group case, I have no comments for that.

P.S. It turns out the main obstruction is that transporting Π-types performs extremely slow. I don't know how to get around it.

[kangxyz]

Emm... I had changed the definition of isFinSet so that cardinality can be computed more efficiently. That's a major shift. Do you think it is reasonable or not? @ecavallo

[ecavallo]

Is it used in many places in the library? If not, I think it's fine to change it.

[kangxyz]

No, almost nowhere.

[kangxyz]

Nice! Using fiberRel is really smart.

[kangxyz]

There are too many files in Data.FinSet so I move everything about finite types into a new fold.

[kangxyz]

It looks much better now! @ecavallo

[ecavallo]

Thanks! This is all great to have in the library.