[ScriptRaccoon]

This PR adds more core-connected categories, i.e. categories that are equivalent to a category with just one object. The purpose is to reduce the number of missing combinations (the work started while this milestone was still active). These categories rarely appear in practice, but the monoids do.

Delooping of the bicyclic monoid

We add $BC$ for the bicyclic monoid $C = \langle p,q : pq = 1 \rangle$. The category $BC$ is the first category in the database that is core-connected and Cauchy complete, but not left cancellative. All properties have been decided.

For the proof that $BC$ is $\aleph_1$-accessible, we prove a more general theorem in a new content page (thanks Claude):

Let $M$ be a monoid such that $M$ is left cancellative or countable, $M$ satisfies the ascending chain condition on principal right ideals, and $BM$ is Cauchy complete. Then $BM$ is $\aleph_1$-accessible.

This also replaces the proof that $BN$ is $\aleph_1$-accessible. Moreover, a slight modification replaces the proof that $BOn$ has $\aleph_1$-filtered colimits:

Let $M$ be a large monoid. Assume that $M$ is left cancellative and satisfies the ascending chain condition on principal right ideals. Then $BM$ has $\aleph_1$-filtered colimits.

Delooping of the double bicyclic monoid

We add $BD$ for $D = \langle f,g,s : fs = gs = 1 \rangle$. It is the first category in the database that is core-connected but does not have reflexive coequalizers. The theorem above shows that $BD$ is both $\aleph_1$-accessible and $\aleph_1$-coaccessible. All properties have been decided.

Countably infinite sets

We add the category of countably infinite sets, a full subcategory of Set. It is equivalent to $BM$, where $M$ is the monoid of all maps $N \to N$. It is an example of a core-connected category without quotients of congruences. This follows from the fact that it has binary products, together with the new implication "core-connected ∧ binary products ∧ quotients of congruences ⟹ trivial". All properties have been decided.

New implications

• core-connected ∧ one-way ⟹ trivial. This makes the assignments of "not one-way" for $BN$ and $BOn$ redundant, which have been removed.
• core-connected ∧ locally essentially small ⟹ essentially small. This makes the assignment of "not locally essentially small" for $BOn$ redundant, which has been removed.
• core-connected ∧ binary products ∧ quotients of congruences ⟹ trivial.
• locally connected ∧ core-connected ⟹ effectice congrunences ∧ quotients of congruences

New combinations

Found 6 unique witnessed combinations by the supplied structures (BC, BD, Set_c_inf):

Directly witnessed:
- core-connected ∧ ¬reflexive coequalizers
- core-connected ∧ ¬coquotients of cocongruences
- core-connected ∧ ¬coreflexive equalizers
- core-connected ∧ ¬effective cocongruences
- core-connected ∧ ¬quotients of congruences

Dually witnessed:
- core-connected ∧ ¬effective congruences

There are no missing combinations left of the form $p \land \neg q$ where one of $p,q$ is core-connected.

Remark: The category of countably infinite sets alone already witnesses all 6 combinations (or their dual).