Add property: ℵ₁-filtered colimits

[ScriptRaccoon]

This PR adds two properties:

• has ℵ₁-filtered colimits
• is ℵ₁-filtered

As for being ℵ₁-filtered, all categories have been decided. For all categories except Sch, the existence of ℵ₁-filtered colimits has been decided.

For the categories Man, Grp_c, and Set_c, the database already contained proofs that they are not ℵ₁-accessible, but these proofs in fact showed that ℵ₁-filtered colimits do not exist. These were quick wins.

To decide the existence of ℵ₁-filtered colimits for various small categories, and to determine their ℵ₁-accessibility, the following theorem has been added together with its (long) proof:

Theorem. If a category is locally finite, essentially countable, and Cauchy complete, then it is ℵ₁-accessible.

In particular, ℵ₁-filtered colimits exist in this case. The theorem implies ℵ₁-accessibility of FinOrd, $\Delta$, FI, FS, and B (which was previously open), as well as FinSet, FinGrp, and FinAb (for which proofs already existed, albeit imprecise ones).

This PR also adds a proof that Sp is ℵ₁-accessible, that BN is ℵ₁-accessible and that BOn has ℵ₁-filtered colimits (although it is not accessible since it is not well-powered). Questions on mathoverflow have shown that FreeAb and Met_c do not have ℵ₁-filtered colimits. In particular, these categories are not ℵ₁-accessible, which has been open before. That being said, this PR already does some of the work for #91.

The only remaining category is Sch, the category of schemes. As of writing this, CatDat does not even record whether it has filtered colimits (presumably not, otherwise ind-schemes would not be a thing). Deciding whether it has ℵ₁-filtered colimits has therefore been postponed, as has already been done for several other properties of this category.

[ScriptRaccoon]

@ykawase5048 Can you perhaps help here?