[ScriptRaccoon]

In this PR, some of the proofs provided by #403 are added. They are also slightly modified and simplified. Also, some leftovers of #373 are handled.

• Ban has effective cocongruences
• FreeAb is not coaccessible
• FreeAb has an extremal cogenerator, namely Z
• F(I)-Set is cototal (more generally, this holds for G-Set for any large group G, see the new Proposition 3 in the content page on cototal algebraic categories)
• $\omega$-Set is not coaccessible
• $\omega$-Set does not have $\aleph_1$-cofiltered limits

As a result, all properties of Ban, FreeAb and F(I)-Set are now decided. 🎉

The only remaining unknown property of $\omega$-Set is accessibility, which is probably independent of ZFC (see this comment).

Coaccessibility

• Simplified proofs: two new content pages contain reusable lemmas about decreasing chains in coaccessible categories and about tail coproducts in extensive categories. The proofs that Met, PMet, Meas, Top_*, Set_≠∅, (Set × Set)_0,fin, FreeAb and $\omega$-Set are not coaccessible, as well as the implication "infinitary extensive + coaccessible ⟹ trivial", now use these lemmas.
• Definitions: the description of "coaccessible" now spells out the definition, and a typo in the description of "ℵ₁-coaccessible" (colimit instead of limit) is fixed.

Cofiltered-limit-stable epimorphisms

• Generalized implication: "countably extensive + cofiltered-limit-stable epimorphisms ⟹ trivial" replaces "elementary topos + countable coproducts + cofiltered-limit-stable epimorphisms ⟹ trivial".
• New implication: "countable coproducts + extensive + locally cartesian closed ⟹ countably extensive". Likewise, the implication to infinitary extensive now assumes coproducts instead of cocompleteness.
• Redundant assignments removed: as a consequence, the unsatisfied property "cofiltered-limit-stable epimorphisms" is now deduced and has been removed from 17 categories, including Top, Cat, Pos, Meas, Haus and the categories of binary relations. Further redundant assignments were removed from Top (not coaccessible), FreeAb (cogenerator) and $\omega$-Set (not essentially small).

[ScriptRaccoon]

FYI @dschepler this PR also decides the remaining properties of $\omega$-Set. Claude finds all the proofs, and I revise and check them.

[ScriptRaccoon]

Here is why the accessibility of $\omega$-Set is probably independent of ZFC. FYI @dschepler

⚠️ This comment has been written by Claude.

Accessible under a strongly compact cardinal. Let $\kappa$ be a strongly compact cardinal. We claim that $\omega$-Set is $\kappa$-accessible.

1. $\omega$-Set has $\kappa$-directed colimits: Let $(D_i)_{i \in I}$ be a $\kappa$-directed diagram in $\omega$-Set, let $X$ be the colimit of the underlying sets, and let $c_i : D_i \to X$ be the colimit maps. The filter on $I$ generated by the sets $\{j \in I \mid j \geq i\}$ is $\kappa$-complete, so it extends to a $\kappa$-complete ultrafilter $U$. We declare that $n$ realizes $x \in X$ if the set of $j \in I$ such that $n$ realizes some preimage of $x$ in $D_j$ belongs to $U$.
   • Each $c_i$ is a morphism: choose a tracker of each transition morphism $D_i \to D_j$ with $j \geq i$. Since there are only countably many partial recursive functions and $U$ is countably complete, there is a $\psi$ such that the set of $j \geq i$ with tracker $\psi$ belongs to $U$. Then $\psi$ tracks $c_i$. In particular, every element of $X$ has a realizer.
   • Universal property: let $f_i : D_i \to Z$ be a cocone with induced function $f : X \to Z$, and choose trackers $\varphi_i$ of $f_i$. As before, there is a $\varphi$ such that the set of $i$ with $\varphi_i = \varphi$ belongs to $U$. If $n$ realizes $x \in X$, there is some $j$ in this set such that $n$ realizes a preimage $a$ of $x$ in $D_j$, and then $\varphi(n)$ realizes $f_j(a) = f(x)$. So $\varphi$ tracks $f$. Uniqueness holds since the forgetful functor is faithful.
2. Every $\omega$-set $Y$ with fewer than $\kappa$ elements is $\kappa$-presentable: Let $g : Y \to X$ be a morphism into the colimit above with tracker $\theta$. As a function, $g$ factors through some $D_i$. For each of the fewer than $\kappa$ pairs $(y,n)$ such that $n$ realizes $y$, the number $\theta(n)$ realizes a preimage of $g(y)$ in $D_j$ for $U$-many $j$. Since $U$ is $\kappa$-complete, there is a single $j \geq i$ that works for all pairs. Fewer than $\kappa$ identifications move these preimages to the factorization in some $D_k$, and the composite of $\theta$ with a tracker of $D_j \to D_k$ tracks the factorization $Y \to D_k$. The injectivity part follows since the forgetful functor is faithful and $Y$ has fewer than $\kappa$ elements.
3. Every $\omega$-set is the $\kappa$-directed colimit of its $\omega$-subsets with fewer than $\kappa$ elements (with the restricted realizers): This holds in ZFC for every uncountable regular cardinal $\kappa$: if no tracker works for the whole $\omega$-set, choose a counterexample for each of the countably many partial recursive functions. These form a countable sub-$\omega$-set whose tracker gives a contradiction.

Since the $\omega$-sets whose underlying set is a cardinal $< \kappa$ form a set, this proves the claim. Hence, if ZFC + "there is a strongly compact cardinal" is consistent, ZFC does not prove that $\omega$-Set is not accessible.

Why ZFC probably does not prove accessibility. The construction above depends on countably complete ultrafilters on $I$ that contain the sets $\{j \in I \mid j \geq i\}$. In L there are no such ultrafilters, since L has no measurable cardinals. The situation is the same as for FreeAb, which is accessible if there are arbitrarily large strongly compact cardinals but not accessible under V = L (see the introduction of Lieberman–Rosický, who refer to Eklof–Mekler), and which is therefore marked as undecidable. Also, van Oosten, whose construction is the basis of our proof for $\aleph_1$-filtered colimits, writes about the related question whether $\nabla :$ Set $\to$ Eff preserves $\lambda$-filtered colimits for larger $\lambda$ that "any result might well depend on axioms independent of ZFC".

What is missing. To mark accessibility as undecidable, we need a model of ZFC, presumably L, in which $\omega$-Set does not have $\kappa$-filtered colimits for any regular cardinal $\kappa$. The counterexample for $\aleph_1$ does not generalize directly. It is a counting argument: $Hom(Y, N)$ is countable for every $\omega$-set $Y$, but the colimit would admit uncountably many morphisms to $N$. For $\kappa \geq \aleph_2$ this cannot work, since every $\kappa$-cofiltered limit of countable sets is countable. A counterexample in L would presumably need $\kappa$-Aronszajn trees for non-weakly compact $\kappa$, and diagrams indexed by $P_\kappa(\lambda)$ for weakly compact $\kappa$. Ideas are welcome.