Dependent sums and products of cardinals

[fredrik-bakke]

Depends on #1591

[lowasser]

I'm excited to see this work; I attempted once or twice to tackle the commutative semiring of cardinalities but didn't get very far.

[fredrik-bakke]

I'm not sure I will complete this work anytime soon, but it's sure been fun to think a little about. Let me know if any of this is blocking your work and I'll make it a priority to merge, or remove it if I will not finish it.

[fredrik-bakke]

Perhaps you would be willing to review #1591, @lowasser? I believe you're in as good a position as anyone to review that PR.

[fredrik-bakke]

This PR has now matured and is very soon ready for review. I'm pleased by the new concepts I introduce in this PR of "cardinality-recursive" and "cardinality-projective" sets. Both contain the finite sets. In particular we may constructively prove Kőnig's theorem for cardinality-projective sets. (EDIT: That will be part of a subsequent PR)

[fredrik-bakke]

Would you be willing to review it when it is done @lowasser?

[fredrik-bakke]

@lowasser It will in total be split into three PRs. The first one is already ready: #1591.