Combinatorics of Finite Sets

[kangrongji]

This PR contains :

• Closure properties of FinSet under several type constructors (e.g., Σ-types, Π-types , type of equivalences);

• A proof of (axiom of) finite choice;

• Adding some requisite definitions to the library.

In theory, one can calculate the cardinality of any combinations of these constructors applied to finite sets and many combinatorial problems can be described in this way. For example, the number of elements in Fin 3 ≃ Fin 3 can be correctly evaluated as 6. Unfortunately, it seems unfeasible even to compute that for Fin 4.

I guess most of the results can be extended to finite groupoids or even finite categories. So the recent works of Egbert Rijke in OEIS-A000001 can be reproduced in cubical agda.

[kangrongji]

I might be too optimistic. There is no way to generalize most of these results to higher types but with one exception, namely the closed-ness under Σ-types. And it is exactly what Rijke needs to construct the number of finite groups.

[mortberg]

Nice! Ping @EgbertRijke

[mortberg]

Great! Thanks for the contribution.

A general remark is that we should reorganize FinSet a bit so that we have a Base file and the Cubical.Data.FinSet file just re-exports things.

Also, I think isFinSet should be called isFinite

[kangrongji]

Great! Thanks for the contribution.

A general remark is that we should reorganize FinSet a bit so that we have a Base file and the Cubical.Data.FinSet file just re-exports things.

Also, I think isFinSet should be called isFinite

Really necessary to reorganize the files. However, I think we should keep the name isFinSet. Finiteness has certain extensions to higher types and someone will probably define something like isFinGroupoid in the near future. Names as isFinite would lead to confusion.

[kangrongji]

Reorganize the files and switch to the library definition of injective/surjective functions. Looks much better now!

[mortberg]

I had a few comments which I already posted, once they are fixed I'll be happy to merge

[mortberg]

Great! Thanks for the contribution.
A general remark is that we should reorganize FinSet a bit so that we have a Base file and the Cubical.Data.FinSet file just re-exports things.
Also, I think isFinSet should be called isFinite

Really necessary to reorganize the files. However, I think we should keep the name isFinSet. Finiteness has certain extensions to higher types and someone will probably define something like isFinGroupoid in the near future. Names as isFinite would lead to confusion.

Ok, I buy this argument! Especially if we move the proof that FinSet A is actually a set to Base

[kangrongji]

I have moved isFinSet→isSet to Base with a direct argument. Fixed the variables naming too.

[kangrongji]

Btw there are so many different aspects of finite sets (e.g. Fin, SumFin, FinInd, FinData) and the definitions are separated in several files/folders. Maybe we should clean & reorganize them for some time and make things more coherent.

[mortberg]

Btw there are so many different aspects of finite sets (e.g. Fin, SumFin, FinInd, FinData) and the definitions are separated in several files/folders. Maybe we should clean & reorganize them for some time and make things more coherent.

Indeed, that would be very welcome in a future PR!

[kangrongji]

Wait, I think I should add some facts about cardinality so that others can do combinatorics immediately.

[mortberg]

I think we should merge this now and any additions come in another PR. It will be much easier for me to review the new stuff that way.

So should I merge?

[kangrongji]

@mortberg It's Ok to merge now. I still need some time to add new stuff.

[mortberg]

Great, thanks for the contribution!