Add an example of a cocomplete category without equalizers

[ScriptRaccoon]

TODO: decide if C^ always has effective cocongruences. if yes, add this to the content page and reference this fact in the proof for the example category.

---

This PR adds an example of a cocomplete category without equalizers, namely the "artificial" example presented in my question MSE/5137415. It is the free cocompletion of a suitably defined locally small but non-small category. I have been waiting for answers with other, more natural examples for a while now, but apparently, they simply do not exist.

All properties of this category have now been decided. Quite a bit of work was necessary to achieve this. Some proofs can be carried out for free cocompletions in general and have therefore been extracted to a separate content page. To show that the category is not concretizable, Isbell's condition for concretizability has been added. Most of the other proofs, however, depend on a concrete description of the small presheaves in this particular situation.

The new category is not just a witness to cocomplete ∧ ¬equalizers, but also to several other property combinations. More precisely, the combinations script (cf. #347) allows us to list 78 new combinations (see below) witnessed by this new category. If we also take the duals into account, the number is even 153. The number of consistent combinations of the form p ∧ ¬q without witnesses has decreased from 886 to 733. This is still a large number, but the reduction is remarkable.

• locally essentially small ∧ ¬concretizable
• cocomplete ∧ ¬binary powers
• cocomplete ∧ ¬binary products
• cocomplete ∧ ¬coequalizers of kernel pairs
• cocomplete ∧ ¬cofiltered limits
• cocomplete ∧ ¬connected limits
• cocomplete ∧ ¬coquotients of cocongruences
• cocomplete ∧ ¬coreflexive equalizers
• cocomplete ∧ ¬cosifted limits
• cocomplete ∧ ¬directed limits
• cocomplete ∧ ¬equalizers
• cocomplete ∧ ¬equalizers of cokernel pairs
• cocomplete ∧ ¬kernel pairs
• cocomplete ∧ ¬pullbacks
• cocomplete ∧ ¬sequential limits
• cocomplete ∧ ¬wide pullbacks
• cocomplete ∧ ¬ℵ₁-cofiltered limits
• filtered-colimit-stable monomorphisms ∧ ¬generating set
• infinitary extensive ∧ ¬binary powers
• infinitary extensive ∧ ¬binary products
• infinitary extensive ∧ ¬coquotients of cocongruences
• infinitary extensive ∧ ¬coreflexive equalizers
• infinitary extensive ∧ ¬countably distributive
• infinitary extensive ∧ ¬distributive
• infinitary extensive ∧ ¬equalizers
• infinitary extensive ∧ ¬finite powers
• infinitary extensive ∧ ¬finite products
• infinitary extensive ∧ ¬finitely complete
• infinitary extensive ∧ ¬infinitary distributive
• infinitary extensive ∧ ¬kernel pairs
• infinitary extensive ∧ ¬parametrized natural numbers object
• infinitary extensive ∧ ¬pullbacks
• co-Malcev ∧ ¬equalizers of cokernel pairs
• effective cocongruences ∧ ¬coquotients of cocongruences
• coproducts ∧ ¬binary powers
• coproducts ∧ ¬binary products
• coproducts ∧ ¬coquotients of cocongruences
• countably extensive ∧ ¬binary powers
• countably extensive ∧ ¬binary products
• countably extensive ∧ ¬coquotients of cocongruences
• countably extensive ∧ ¬countably distributive
• countably extensive ∧ ¬distributive
• countably extensive ∧ ¬finite powers
• countably extensive ∧ ¬finite products
• countably extensive ∧ ¬parametrized natural numbers object
• connected colimits ∧ ¬equalizers of cokernel pairs
• multi-cocomplete ∧ ¬coequalizers of kernel pairs
• multi-cocomplete ∧ ¬cofiltered limits
• multi-cocomplete ∧ ¬connected limits
• multi-cocomplete ∧ ¬coquotients of cocongruences
• multi-cocomplete ∧ ¬coreflexive equalizers
• multi-cocomplete ∧ ¬cosifted limits
• multi-cocomplete ∧ ¬directed limits
• multi-cocomplete ∧ ¬equalizers
• multi-cocomplete ∧ ¬kernel pairs
• multi-cocomplete ∧ ¬pullbacks
• multi-cocomplete ∧ ¬sequential limits
• multi-cocomplete ∧ ¬wide pullbacks
• multi-cocomplete ∧ ¬ℵ₁-cofiltered limits
• countable coproducts ∧ ¬binary powers
• countable coproducts ∧ ¬binary products
• extensive ∧ ¬coquotients of cocongruences
• copowers ∧ ¬binary powers
• copowers ∧ ¬binary products
• copowers ∧ ¬coquotients of cocongruences
• ℵ₂-small coproducts ∧ ¬binary powers
• ℵ₂-small coproducts ∧ ¬binary products
• ℵ₂-small coproducts ∧ ¬coquotients of cocongruences
• wide pushouts ∧ ¬equalizers of cokernel pairs
• strict initial object ∧ ¬coquotients of cocongruences
• ℵ₂-small copowers ∧ ¬binary powers
• ℵ₂-small copowers ∧ ¬binary products
• ℵ₂-small copowers ∧ ¬coquotients of cocongruences
• countable copowers ∧ ¬binary powers
• countable copowers ∧ ¬binary products
• disjoint coproducts ∧ ¬binary powers
• disjoint coproducts ∧ ¬binary products
• disjoint coproducts ∧ ¬coquotients of cocongruences