Variants of the category of finite sets

[ScriptRaccoon]

The goal of this PR and other recent PRs (such as #340 and #350) is to add categories that satisfy a (consistent) property combination of the form "p and not q" that has not been witnessed before (milestone). (There have already been several corresponding PRs for functors, for example #306.) The unwitnessed combinations of this type are listed on the page /missing.

Usually, the weirder a category, the more new property combinations it witnesses. Even though these categories are not very interesting in their own right, it makes sense to add them to illustrate which property combinations are possible.

Specifically, this PR adds three categories:

• FinSet_even (finite sets with even cardinality)
• FinSet_odd (finite sets with odd cardinality)
• FinSet_3^k (finite sets with cardinality a power of 3)

Here, FinSet_even (and FinSet_odd) is an example of a category with kernel pairs that is not Cauchy complete, and FinSet_3^k (and FinSet_odd) is an example of a cartesian closed category without binary copowers. These property combinations are new. All properties of these new categories have been decided.

New combinations

However, these categories satisfy many more new combinations. The combinations script (cf. #352) shows 34 new combinations.

pnpm db:combinations category FinSet_even FinSet_odd FinSet_power_3

prints:

Found 34 unique witnessed combinations by the supplied structures (FinSet_even, FinSet_odd, FinSet_power_3):

Directly witnessed:
- kernel pairs ∧ ¬Cauchy complete
- strict initial object ∧ ¬Cauchy complete
- essentially countable ∧ ¬quotients of congruences
- locally finite ∧ ¬quotients of congruences
- cartesian closed ∧ ¬Cauchy complete
- cartesian closed ∧ ¬binary copowers
- cartesian closed ∧ ¬binary coproducts
- cartesian closed ∧ ¬coequalizers
- cartesian closed ∧ ¬coequalizers of kernel pairs
- cartesian closed ∧ ¬cokernel pairs
- cartesian closed ∧ ¬equalizers of cokernel pairs
- disjoint finite products ∧ ¬natural numbers object
- cartesian closed ∧ ¬pushouts
- cartesian closed ∧ ¬quotients of congruences
- cartesian closed ∧ ¬reflexive coequalizers
- cartesian closed ∧ ¬ℵ₁-accessible
- cartesian closed ∧ ¬ℵ₁-filtered colimits
- cartesian closed ∧ ¬kernel pairs

Dually witnessed:
- cokernel pairs ∧ ¬Cauchy complete
- strict terminal object ∧ ¬Cauchy complete
- essentially countable ∧ ¬coquotients of cocongruences
- locally finite ∧ ¬coquotients of cocongruences
- cocartesian coclosed ∧ ¬Cauchy complete
- cocartesian coclosed ∧ ¬binary powers
- cocartesian coclosed ∧ ¬binary products
- cocartesian coclosed ∧ ¬equalizers
- cocartesian coclosed ∧ ¬equalizers of cokernel pairs
- cocartesian coclosed ∧ ¬kernel pairs
- cocartesian coclosed ∧ ¬coequalizers of kernel pairs
- cocartesian coclosed ∧ ¬pullbacks
- cocartesian coclosed ∧ ¬coquotients of cocongruences
- cocartesian coclosed ∧ ¬coreflexive equalizers
- cocartesian coclosed ∧ ¬ℵ₁-cofiltered limits
- cocartesian coclosed ∧ ¬cokernel pairs

As a result, the number of unwitnessed consistent combinations went down from 735 to 701. It is still a long way ...

Oddness

Actually, without FinSet_odd, the number would be the same, but this is just because of the other two new categories. Without them, FinSet_odd already witnesses 30 new combinations. Interestingly, there is just one property that distinguishes FinSet_odd and FinSet_3^k: whereas FinSet_odd has kernel pairs, FinSet_3^k does not have kernel pairs.

It's also interesting to look at the comparison table of the three new categories.