diff --git a/.cspell.json b/.cspell.json
index e3a2b1ce..5243af72 100644
--- a/.cspell.json
+++ b/.cspell.json
@@ -65,6 +65,7 @@
"cocomplete",
"cocompleteness",
"cocompletion",
+ "cocompletions",
"cocone",
"cocones",
"cocongruence",
@@ -215,6 +216,7 @@
"Kerodon",
"Kolmogorov",
"Kunen",
+ "Kuratowski",
"Lawvere",
"libsql",
"Lindelöf",
diff --git a/content/free-cocompletion.md b/content/free-cocompletion.md
new file mode 100644
index 00000000..8aef720c
--- /dev/null
+++ b/content/free-cocompletion.md
@@ -0,0 +1,165 @@
+---
+title: The free cocompletion of a locally small category
+description: We investigate the properties of the free cocompletion of a locally small category.
+---
+
+## The free cocompletion of a locally small category
+
+Let $\C$ be a locally small category. All results here can easily be adapted to the case that $\C$ is locally essentially small, and we do not assume that $\C$ is small. Then $\widehat{\C}$ denotes its _free cocompletion_ (often called $P\C$ in the literature when $\C$ is not assumed to be small), which is the full subcategory of $[\C^{\op},\Set]$ consisting presheaves
+$$F : \C^{\op} \to \Set$$
+that are _small_. This condition can be described in many equivalent ways:
+
+1. $F$ is a small colimit of representable functors.
+2. There is a small category $\I$ such that $F$ is the left Kan extension of a presheaf on $\I$ along a functor $\I \to \C$.
+3. There is small subcategory $\I \subseteq \C$ such that $F$ is the left Kan extension of its restriction to $\I$.
+4. The category of elements $\int F$ is [finally small](https://ncatlab.org/nlab/show/finally+small).
+
+Here, the objects of $\int F$ are pairs $(X,a)$, where $X \in \C$ and $a \in F(X)$, and a morphism $(X,a) \to (Y,b)$ is a morphism $f : X \to Y$ with $F(f)(b) = a$. The equivalence of the conditions (1), (2), (3) is proven as Proposition 4.83 in Kelly's book [Basic Concepts of Enriched Category Theory](http://www.tac.mta.ca/tac/reprints/articles/10/tr10.html). The implication (1) $\implies$ (4) is proven as Proposition 3.7 in Kan Extensions are Partial Colimits by Perrone-Tholen (but there must be earlier references). The implication (4) $\implies$ (1) follows from the [co-Yoneda Lemma](https://ncatlab.org/nlab/show/co-Yoneda+lemma)
+$$F \cong \colim_{(X,a) \in \int F} \Hom(-,X)$$
+and the fact that final functors do not "change" colimits; see Proposition 2.5.2 in Kashiwara-Schapira.
+
+In contrast to the full presheaf category $[\C^{\op},\Set]$, its subcategory $\widehat{\C}$ of small presheaves is always locally essentially small:
+
+::: Lemma 1
+If $\C$ is a locally small category, then $\widehat{\C}$ is locally essentially small.
+:::
+
+::: Proof
+Let $F : \C^{\op} \to \Set$ be a small presheaf, so that $F \cong \colim_i \Hom(-,X_i)$ for a small diagram $X : \I \to \C$. For every other (small) presheaf $G : \C^{\op} \to \Set$ we compute, using the Yoneda Lemma,
+$$\textstyle \Hom(F,G) \cong \lim_i \Hom(\Hom(-,X_i),G) \cong \lim_i G(X_i),$$
+and the latter is a set.
+:::
+
+But it is usually not locally small:
+
+::: Lemma 2
+If $\widehat{\C}$ is locally small, then $\C$ is small.
+:::
+
+Disclaimer: This result and its proof are not relevant for category theory and are also depending on implementation details of set theory. That $\widehat{\C}$ is locally essentially small is only what matters.
+
+::: Proof
+If $\C$ is empty, there is nothing to prove. Otherwise, choose an object $X \in \C$. Consider the collection of morphisms $\Hom(-,X) \to \Hom(-,X)$, which is surely isomorphic to the set $\Hom(X,X)$. By assumption, it actually _is_ a set. It follows that $\{\id_{\Hom(-,X)}\}$ is a set, and therefore also that $\id_{\Hom(-,X)}$ is a set. This natural transformation is a map that associates to every object $Y \in \Ob(\C)$ the map $\id_{\Hom(Y,X)}$. If we model a map as a set of ordered pairs and ordered pairs as Kuratowski pairs, we get
+
+$$
+\begin{align*}
+\id_{\Hom(-,X)} & = \bigl\{(Y,\id_{\Hom(Y,X)}) : Y \in \Ob(\C)\bigr\} \\
+& = \bigl\{\{\{Y\},\{Y,\id_{\Hom(Y,X)}\}\} : Y \in \Ob(\C)\bigr\}
+\end{align*}
+$$
+
+This construction shows $\Ob(\C) \subseteq \bigcup \bigcup \id_{\Hom(-,X)}$, so that $\Ob(\C)$ is indeed a set.
+:::
+
+::: Lemma 3
+If $\C$ is a locally small category, then $\widehat{\C}$ is cocomplete. Colimits can be constructed objectwise.
+:::
+
+::: Proof
+This follows from cocompleteness of $[\C^{\op},\Set]$ with objectwise constructed colimits and the third characterization of small presheaves above. Details can be found as Proposition 5.34 in Kelly's book.
+:::
+
+The existence of limits in $\widehat{\C}$ is a much more complicated issue, see the paper [_Limits of small functors_](https://arxiv.org/pdf/math/0610439) by Day-Lack. The following result is useful in this regard. Namely, it shows that $\widehat{\C}$ has limits of a given type if and only if small functors are closed under these limits taken in the category of all presheaves.
+
+::: Lemma 4
+For every $X \in \C$ the evaluation functor $\ev_X : \widehat{\C} \to \Set$, $F \mapsto F(X)$ is continuous. In particular, the inclusion functor $\widehat{\C} \hookrightarrow [\C^{\op},\Set]$ is continuous, and every limit that exists in $\widehat{\C}$ is an objectwise limit.
+:::
+
+::: Proof
+By the Yoneda Lemma, the evaluation functor is represented by $\Hom(-,X)$. Thus, it is continuous.
+:::
+
+::: Lemma 5
+A morphism $\alpha : F \to G$ in $\widehat{\C}$ is a monomorphism (resp. epimorphism) if and only if for every $X \in \C$ the map $\alpha(X) : F(X) \to G(X)$ injective (resp. surjective).
+:::
+
+::: Proof
+The direction $\impliedby$ is trivial in each case. For the direction $\implies$, the evaluation functor $\ev_X : \widehat{\C} \to \Set$ is continuous by Lemma 4 and therefore preserves monomorphisms. Furthermore, it is also cocontinuous by Lemma 3 and therefore preserves epimorphisms.
+:::
+
+::: Lemma 6
+If $\C$ is a locally small category, then $\widehat{\C}$ is mono-regular. Actually, every monomorphism is an effective monomorphism. Moreover, monomorphisms are stable under filtered colimits.
+:::
+
+::: Proof
+The first statement is a formal consequence of the fact that every monomorphism in $\Set$ is effective and the already established facts that monomorphisms and pushouts can be understood objectwise. For similar reasons, the second statement is a formal consequence of the corresponding fact for $\Set$.
+:::
+
+::: Lemma 7
+If $\C$ is a locally small category, then $\widehat{\C}$ is infinitary extensive.
+:::
+
+::: Proof
+We need to prove that for a family of small presheaves $(P_i)_{i \in I}$ the coproduct functor
+$$\textstyle \prod_{i \in I} \widehat{\C} / P_i \to \widehat{\C}/\coprod_{i \in I} P_i$$
+is an equivalence of categories. Since $\Set$ is infinitary extensive, also $[\C^{\op},\Set]$ is infinitary extensive, so that the coproduct functor
+$$\textstyle \prod_{i \in I} [\C^{\op},\Set] / P_i \to [\C^{\op},\Set]/\coprod_{i \in I} P_i$$
+is an equivalence of categories. Since $\widehat{\C}$ is a full subcategory of $[\C^{\op},\Set]$ that is closed under coproducts, it remains to prove that if a coproduct of presheaves $\coprod_{i \in I} F_i$ is small, then each $F_i$ is small. For this, it suffices to prove for two presheaves $F,G$ for which $F+G$ is small, that $F$ is small. The category of elements $\int (F+G)$ identifies with $\int F + \int G$. Thus, the claim follows from the next lemma.
+:::
+
+::: Lemma 8
+Let $\C,\D$ be two categories. Assume that the coproduct $\C + \D$ is finally small. Then $\C$ is finally small.
+:::
+
+::: Proof
+Assume that $\I \to \C + \D$ is a final functor, where $\I$ is small. Since $\Cat$ is extensive, we get a decomposition $\I = \I_\C + \I_\D$ with two functors $\I_\C \to \C$ and $\I_\D \to \D$. For every $X \in \C$ the comma category $X \downarrow I_\C$ identifies with the comma category $X \downarrow I$, which is connected. Therefore, $I_\C \to \C$ is final.
+:::
+
+::: Lemma 9
+Let $\C$ be a locally small category. Then $\widehat{\C}$ is co-Malcev.
+:::
+
+::: Proof
+This follows since $\Set$ is co-Malcev and since finite colimits are objectwise.
+:::
+
+::: Proposition 10
+Let $\C$ be a locally small category. Then $\widehat{\C}$ is epi-regular.
+:::
+
+Notice that this would be easy if $\widehat{\C}$ has pullbacks. In that case, every epimorphism would even be effective since this is the case for $\Set$. But in general, $\widehat{\C}$ may fail to have pullbacks. This is why the proof is more complicated.
+
+::: Proof
+First, notice that the Yoneda Lemma and the description of epimorphisms (see Lemma 5) implies that representable functors are [projective objects](https://ncatlab.org/nlab/show/projective+object). Therefore, also coproducts of representable functors are projective.
+
+Now let $\eta : F \to G$ be an epimorphism of small presheaves. Since $F$ is small, there is an epimorphism
+$$F_0 \xrightarrow{~ \pi ~} F,$$
+where $F_0$ is a coproduct of representable functors. Since $G$ is small, there is a coequalizer diagram
+
+$$
+G_1
+\begin{array}{c}
+\xrightarrow{~ \alpha ~ }\\[-1.25ex] \xrightarrow[~ \beta ~ ]{}
+\end{array}
+G_0 \xrightarrow{~ \psi ~} G,
+$$
+
+where $G_0$ and $G_1$ are coproducts of representable functors. Since $G_0$ is projective, there is a morphism $\lambda : G_0 \to F$ such that $\eta \circ \lambda = \psi$. Since $F_0$ is projective, there is a morphism $\mu : F_0 \to G_0$ such that $\psi \circ \mu = \eta \circ \pi$. We get the following diagram, where the outer square and the lower triangle commutes, but not necessarily the upper triangle.
+
+$$
+\begin{CD}
+F_0 @>{\pi}>> F \\
+@V{\mu}VV \, \, \nearrow{\scriptsize \, \lambda} @VV{\eta}V \\
+G_0 @>>{\psi}> G
+\end{CD}
+$$
+
+Define the morphisms $\gamma,\delta : G_1 \sqcup F_0 \rightrightarrows F$ by
+$$\gamma|_{G_1} = \lambda \circ \alpha, \quad \delta|_{G_1} = \lambda \circ \beta,$$
+$$\gamma|_{F_0} = \lambda \circ \mu, \quad \delta|_{F_0} = \pi.$$
+We will prove that $\eta : F \to G$ is a coequalizer of $\gamma$ and $\delta$. First, $\eta$ coequalizes these because
+$$\eta \circ \gamma|_{G_1} = \eta \circ \lambda \circ \alpha = \psi \circ \alpha = \psi \circ \beta = \eta \circ \lambda \circ \beta = \eta \circ \delta|_{G_1}$$
+and
+$$\eta \circ \gamma|_{F_0} = \eta \circ \lambda \circ \mu = \psi \circ \mu = \eta \circ \pi = \eta \circ \delta|_{F_0}.$$
+Conversely, suppose that $\vartheta : F \to H$ is a morphism that coequalizes these morphisms, meaning that $\vartheta \circ \lambda \circ \alpha = \vartheta \circ \lambda \circ \beta$ and $\vartheta \circ \lambda \circ \mu = \vartheta \circ \pi$. The first equation means that there is a morphism $\vartheta' : G \to H$ such that $\vartheta' \circ \psi = \vartheta \circ \lambda$. The second equation then becomes
+$$\vartheta \circ \pi = \vartheta' \circ \psi \circ \mu = \vartheta' \circ \eta \circ \pi,$$
+which is equivalent to $\vartheta = \vartheta' \circ \eta$. We have thus shown that every morphism that coequalizes $\alpha$ and $\beta$ factors through $\eta$, and uniqueness is clear since $\eta$ is an epimorphism.
+:::
+
+::: Lemma 11
+Let $\C$ be a locally small category. Then $\widehat{\C}$ has effective congruences.
+:::
+
+::: Proof
+Let $f,g : F \rightrightarrows G$ be a congruence in $\widehat{\C}$. Let $p : G \twoheadrightarrow Q$ be its quotient (i.e. coequalizer) in $\widehat{\C}$, which is constructed objectwise. Applying the functorial definition of a congruence to representable functors in $\widehat{\C}$, we see that for every object $X \in \C$ that $f(X),g(X) : F(X) \rightrightarrows G(X)$ is a congruence in $\Set$. Since congruences in $\Set$ are effective, $f(X),g(X)$ is the kernel pair of $p(X)$; we are also using [this result](/content/effective-congruence-quotients). Therefore, $f,g$ is the kernel pair of $p$ in the category of all presheaves, _a fortiori_ in the category of small presheaves.
+:::
diff --git a/content/nice-and-small-presheaves.md b/content/nice-and-small-presheaves.md
new file mode 100644
index 00000000..17df2039
--- /dev/null
+++ b/content/nice-and-small-presheaves.md
@@ -0,0 +1,70 @@
+---
+title: Nice and small presheaves
+description: We give a concrete description of small presheaves on a specific locally small category.
+---
+
+## Nice and small presheaves
+
+Let $\C$ be the locally small category defined in [this entry](/category/example-cocomplete-no-equalizers). Its objects are $A$, $B$, and every set $X$. The non-identity morphisms are $f,g : A \rightrightarrows B$, $u_X : X \to A$ and $v_X : X \to B$ for every set $X$, and they satisfy the relation $f \circ u_X = g \circ u_X = v_X$.
+
+Let $F$ be a presheaf on $\C$. Concretely, this means that we are given sets $F(A)$, $F(B)$, and $F(X)$ for every set $X$, two maps $f^*,g^* : F(B) \rightrightarrows F(A)$ and, for every set $X$, a map $u_X^* : F(A) \to F(X)$ satisfying
+$$u_X^* \circ f^* = u_X^* \circ g^* = v_X^*,$$
+where $v_X^* : F(B) \to F(X)$. Thus, we have a commutative diagram
+$$F(B) ~\overset{f^*}{\underset{g^*}{\rightrightarrows}}~ F(A) \xrightarrow{u_X^*} F(X).$$
+If this is a coequalizer diagram, we say that $F$ is _nice at_ $X$. In particular, $u_X^*$ must be surjective. We say that $F$ is _nice_ if there is a set $S_F$ of sets such that $F$ is nice at every set $X \notin S_F$. We then call $S_F$ an _exceptional set_ for $F$. Intuitively, this means that $F$ is nice "almost everywhere".
+
+Let us determine which representable presheaves are nice.
+
+1. When $F = \Hom(-,A)$, the diagram evaluates to
+ $$\varnothing ~\overset{f^*}{\underset{g^*}{\rightrightarrows}}~ \{\id_A\} \xrightarrow{u_X^*} \{u_X\},$$
+ which is clearly a coequalizer diagram. Thus, this presheaf is nice everywhere.
+
+2. When $F = \Hom(-,B)$, the diagram evaluates to
+ $$\{\id_B\} ~\overset{f^*}{\underset{g^*}{\rightrightarrows}}~ \{f,g\} \xrightarrow{u_X^*} \{v_X\},$$
+ which is again clearly a coequalizer diagram. Thus, this presheaf is nice everywhere.
+
+3. When $F = \Hom(-,X)$ for a set $X$, the diagram at $X$ is
+ $$\varnothing ~\overset{f^*}{\underset{g^*}{\rightrightarrows}}~ \varnothing \xrightarrow{u_X^*} \{\id_X\},$$
+ which is not a coequalizer diagram. At $Y \neq X$, however, the diagram evaluates to
+ $$\varnothing ~\overset{f^*}{\underset{g^*}{\rightrightarrows}}~ \varnothing \xrightarrow{u_Y^*} \varnothing,$$
+ and is therefore a coequalizer diagram. Hence, the set $\{X\}$ is an exceptional set for $\Hom(-,X)$.
+
+::: Lemma
+A presheaf $F$ on $\C$ is small if and only if it is nice.
+:::
+
+::: Proof
+The collection of nice presheaves is clearly closed under small colimits of presheaves, since colimits commute with colimits and colimits of presheaves are computed objectwise. Furthermore, we have seen above that representable presheaves are nice. It follows that every small presheaf is nice.
+
+Conversely, assume that $F$ is a nice presheaf and choose an exceptional set $S_F$. To show that $F$ is small, we will show that its category of elements $\int F$ has a small final subcategory. Let $\D$ be the full subcategory of $\int F$ consisting of the objects
+
+- $(A,a)$ for $a \in F(A)$,
+- $(B,b)$ for $b \in F(B)$,
+- $(X,x)$ for $x \in F(X)$ and $X \in S_F$.
+
+This is a small category since $S_F$ is a set.
+
+We need to show that, for every object $T \in \int F$, the comma category $T \downarrow \D$ is connected. This is trivial for objects $T$ of $\D$. It remains to check this for $(X,x)$, where $x \in F(X)$ and $X \notin S_F$. By the definition of $S_F$, the diagram
+$$F(B) ~\overset{f^*}{\underset{g^*}{\rightrightarrows}}~ F(A) \xrightarrow{u_X^*} F(X) \tag{1}$$
+is a coequalizer diagram. In particular, $u_X^*$ is surjective, so there is some $a \in F(A)$ with $u_X^*(a) = x$. Then $u_X : (X,x) \to (A,a)$ is a morphism in $\int F$, showing that $(X,x) \downarrow \D$ is non-empty.
+
+There are two types of objects in $(X,x) \downarrow \D$. The first type consists of morphisms
+$$u_X : (X,x) \to (A,a),$$
+where $a \in F(A)$ satisfies $u_X^*(a)=x$. The second type consists of morphisms
+$$v_X : (X,x) \to (B,b),$$
+where $b \in F(B)$ satisfies $v_X^*(b)=x$. Every object of the second type is connected to an object of the first type, since $f : (A,f^*(b)) \to (B,b)$ is a morphism with $f \circ u_X = v_X$.
+
+It remains to show that every two objects
+$$(X,x) \to (A,a), \quad (X,x) \to (A,a')$$
+are connected, where $a,a' \in F(A)$ satisfy $u_X^*(a)=u_X^*(a')=x$. Since the diagram $(1)$ is a coequalizer diagram, there is a finite sequence of elements $a_0,\dotsc,a_n$ in $F(A)$, where $a_0=a$ and $a_n=a'$, and a finite sequence of elements $b_0,\dotsc,b_{n-1} \in F(B)$ such that, for every $0 \leq i < n$, either
+$$a_i=f^*(b_i), \quad a_{i+1}=g^*(b_i),$$
+or
+$$a_i=g^*(b_i), \quad a_{i+1}=f^*(b_i).$$
+It suffices to show that $(X,x) \to (A,a_i)$ and $(X,x) \to (A,a_{i+1})$ are connected. We may assume without loss of generality that
+$$a_i=f^*(b_i), \quad a_{i+1}=g^*(b_i).$$
+But then both are connected to $(X,x) \to (B,b_i)$ via the morphisms
+
+$$f : (A,a_i) \to (B,b_i), \quad g : (A,a_{i+1}) \to (B,b_i),$$
+
+respectively.
+:::
diff --git a/database/data/categories/Sp.yaml b/database/data/categories/Sp.yaml
index b43eeec4..7187a858 100644
--- a/database/data/categories/Sp.yaml
+++ b/database/data/categories/Sp.yaml
@@ -40,7 +40,7 @@ unsatisfied_properties:
proof: If $1$ denotes the terminal species, there are infinitely many morphisms $1 \to 1 \sqcup 1$ since they correspond to functions $\IN \to \{1,2\}$.
- property: locally small
- proof: 'Disclaimer: This result and its proof are not relevant for category theory and are also depending on the concrete model of set theory. That this category is locally essentially small is only what matters. Now, consider the terminal species $F=G=1$. Then $\Hom(F,G)$ has just a single element, namely the natural transformation $\alpha$ that sends every finite set $X$ to the unique map $\alpha_X : 1 \to 1$. Formally, $\alpha$ is a map, modelled as a set of ordered pairs $(X,\id_1)$, where $X$ is a finite set. Hence, $\alpha$ is not a set (since finite sets do not form a set), and therefore $\Hom(F,G) = \{\alpha\}$ is also not a set.'
+ proof: Since $\FinSet$ is not small, this follows exactly like Lemma 2 here; but this result is not really relevant and what only matters is that $\Sp$ is locally essentially small.
- property: essentially countable
proof: 'Any function $f : \IN \to \IN$ can be regarded as a combinatorial species with trivial actions, and distinct functions yield non-isomorphic species.'
diff --git a/database/data/categories/example-cocomplete-no-equalizers.yaml b/database/data/categories/example-cocomplete-no-equalizers.yaml
new file mode 100644
index 00000000..c8353151
--- /dev/null
+++ b/database/data/categories/example-cocomplete-no-equalizers.yaml
@@ -0,0 +1,188 @@
+id: example-cocomplete-no-equalizers
+name: example of a cocomplete category without equalizers
+notation: $\widehat{\C}$
+objects: small presheaves on a suitable large category (see below)
+morphisms: natural transformations
+description: >-
+ This rather technical and artificial category has solely been added as an example of a cocomplete category that does not have equalizers.
+
+ To construct it, we start with the category $\C$ that has two objects $A,B$ and every set $X$ as an object. (Instead of the collection of sets, we can take any other non-small collection.) There are the identities, two morphisms $f,g : A \rightrightarrows B$, a unique morphism $u_X : X \to A$ for every set $X$, and a unique morphism $v_X : X \to B$ for every set $X$. The composition is defined by $f \circ u_X = g \circ u_X = v_X$. There are no morphisms between distinct sets.
+ $$\begin{array}{c}
+ X \\[0.25ex]
+ {\raisebox{1ex}{$\scriptstyle u_X$}} \!\! \swarrow
+ \qquad
+ \searrow \!\! {\raisebox{1ex}{$\scriptstyle v_X$}} \\
+ A \;\;
+ \begin{array}{c}
+ \xrightarrow{\quad f \quad }\\[-1.25ex]
+ \xrightarrow[\quad g \quad ]{}
+ \end{array}
+ \;\; B
+ \end{array}$$
+ The category in this entry is the free cocompletion $\widehat{\C}$. It consists of small presheaves $F : \C^{\op} \to \Set$, i.e. those presheaves that can be written as a small colimit of representable functors. See here for a couple of equivalent characterizations that hold for general $\C$, as well as general results on free cocompletions, and see here for a concrete description of small presheaves in this specific setting.
+nlab_link: null
+tags:
+ - category theory
+
+related: []
+
+comments:
+ - This category was suggested by Simon Henry in MO/509754 and further explained in MSE/5137415.
+
+satisfied_properties:
+ - property: locally essentially small
+ proof: See Lemma 1 here.
+
+ - property: cocomplete
+ check_redundancy: false
+ proof: Colimits can be constructed objectwise by Lemma 3 here. Alternatively, this follows easily from the description of small presheaves.
+
+ - property: terminal object
+ label: terminal_presheaf_small
+ proof: >-
+ It suffices to check that the terminal presheaf is small. This follows immediately from the description of small presheaves, since in fact, for every set $X$, the diagram
+ $$1 ~\overset{f^*}{\underset{g^*}{\rightrightarrows}}~ 1 \xrightarrow{u_X^*} 1$$
+ is a coequalizer diagram. Alternatively, one can easily check that the terminal presheaf is a coequalizer of $f_*,g_* : \Hom(-,A) \rightrightarrows \Hom(-,B)$, which directly implies that it is small.
+
+ - property: epi-regular
+ proof: See Proposition 10 here.
+
+ - property: filtered-colimit-stable monomorphisms
+ proof: See Lemma 6 here.
+
+ - property: infinitary extensive
+ proof: See Lemma 7 here.
+
+ - property: co-Malcev
+ proof: See Lemma 9 here.
+
+ - property: effective congruences
+ proof: See Lemma 11 here.
+
+ # - property: effective cocongruences
+ # proof: TBA
+
+unsatisfied_properties:
+ - property: skeletal
+ proof: This is trivial.
+
+ - property: locally small
+ proof: Since $\C$ is not small, this follows from Lemma 2 here; however, this result is not really relevant, and all that matters is that $\widehat{\C}$ is locally essentially small.
+
+ - property: semi-strongly connected
+ proof: Pick two different sets $X$ and $Y$. There is no morphism $\Hom(-,X) \to \Hom(-,Y)$, since the image of $\id_X$ would be a morphism $X \to Y$, which does not exist. Likewise, there is no morphism in the other direction.
+
+ - property: well-powered
+ references:
+ - terminal_presheaf_small
+ proof: We already know that the terminal presheaf $1$ is small. For every set $X$, the unique morphism $\Hom(-,X) \to 1$ is a monomorphism since $X$ is subterminal in $\C$ (in fact, any morphism with codomain $X$ is the identity). For different sets $X,X'$ we have $\Hom(-,X) \not\cong \Hom(-,X')$ since there is not even a morphism $X \to X'$ in $\C$. This shows that $\Sub(1)$ is not small.
+
+ - property: well-copowered
+ proof: >-
+ For every set $X$, we use $u_X : X \to A$ to construct the pushout
+ $$P_X \coloneqq \Hom(-,A) \sqcup_{\Hom(-,X)} \Hom(-,A).$$
+ It is a quotient of $\Hom(-,A) \sqcup \Hom(-,A)$. For $X \neq Y$ we have $P_X \not\cong P_Y$ because $P_X(Y)$ has two elements, the two copies of $u_Y$, whereas $P_Y(Y)$ has exactly one element, the image of $u_Y$.
+
+ - property: equalizers
+ proof: >-
+ By Lemma 4 here, it suffices to find parallel morphisms of small presheaves whose equalizer in the category of all presheaves is not small. For example, consider the morphisms $f_*,g_* : \Hom(-,A) \rightrightarrows \Hom(-,B)$. Their equalizer $E$ satisfies $E(X) = \{u_X\}$ for every set $X$, $E(A) = \varnothing$, and $E(B) = \varnothing$. In particular, $u_X^* : E(A) \to E(X)$ is never surjective. Therefore, the description of small presheaves shows that $E$ is not small.
+ label: free_cocompletion_no_equalizers
+ check_redundancy: false # because the counterexample for equalizers of cokernel pairs below is more complicated
+
+ - property: binary powers
+ proof: >-
+ By Lemma 4 here, it suffices to find a small presheaf $F$ whose square $F^2$ in the category of all presheaves is not small. Specifically, we will show that the square $\Hom(-,B)^2$ is not small. By the description of small presheaves, it is sufficient to show that for every set $X$ the diagram
+ $$\Hom(B,B)^2 ~\overset{f^*}{\underset{g^*}{\rightrightarrows}}~ \Hom(A,B)^2 \xrightarrow{u_X^*} \Hom(X,B)^2$$
+ is not a coequalizer diagram. It identifies with
+ $$\{(\id_B,\id_B)\} ~\overset{f^*}{\underset{g^*}{\rightrightarrows}}~ \{f,g\}^2 \xrightarrow{u_X^*} \{(v_X,v_X)\}.$$
+ But the coequalizer of $f^*,g^*$ has three elements, so it cannot be isomorphic to $\{(v_X,v_X)\}$, which has just one element.
+
+ - property: sequential limits
+ proof: >-
+ By Lemma 4 here, it suffices to find a sequence of small presheaves on $\C$ whose limit in the category of all presheaves is not small.
+
+ For $n \in \IN$ define the presheaf $F_n$ on objects by
+ $$F_n(A) = F_n(B) = \IN_{\geq n}, \quad F_n(X)=\{\ast\}$$
+ for every set $X$. The maps $u_X^* : F_n(A) \to F_n(X)$ and $v_X^* : F_n(B) \to F_n(X)$ are uniquely determined. The map $f^* : F_n(B) \to F_n(A)$ is the identity map, while the map $g^* : F_n(B) \to F_n(A)$ is defined by $k \mapsto k + 1$. This is indeed a presheaf since $F_n(X)$ is a singleton. That $F_n$ is small follows from the description of small presheaves, since for every set $X$
+ $$\IN_{\geq n} ~\overset{k \mapsto k}{\underset{k \mapsto k+1}{\rightrightarrows}}~ \IN_{\geq n} \xrightarrow{!} \{\ast\}$$
+ is a coequalizer diagram; there is exactly one equivalence class under $k \sim k+1$ on $\IN_{\geq n}$.
+
+ Define the morphism $F_{n+1} \to F_n$ as the inclusion at $A$ and $B$ and as the identity at $X$. Naturality is easy to check. Let $F_\infty$ denote the limit presheaf of this sequence. We compute $F_\infty(A) = \bigcap_{n \in \IN} \IN_{\geq n} = \varnothing$. Likewise, we have $F_\infty(B) = \varnothing$. But we have $F_\infty(X) = \{\ast\}$. Thus, for every set $X$, the map $u_X^* : F_\infty(A) \to F_\infty(X)$ is not surjective, so the description of small presheaves shows that $F_\infty$ is not small.
+
+ - property: ℵ₁-cofiltered limits
+ references:
+ - free_cocompletion_no_equalizers
+ proof: >-
+ More generally, for every regular cardinal $\kappa$, $\kappa$-sequential and hence also $\kappa$-cofiltered limits do not exist. By Lemma 4 here, it suffices to find a $\kappa$-sequence in $\widehat{\C}$ whose presheaf limit is not small.
+
+ For an ordinal $\alpha < \kappa$, let $T_\alpha \coloneqq [\alpha,\kappa)$ be the set of ordinals greater than or equal to $\alpha$ and less than $\kappa$. For $\beta \leq \alpha$, there is an inclusion map $T_\alpha \to T_\beta$. Notice that
+ $$\textstyle \lim_\alpha T_\alpha = \bigcap_{\alpha < \kappa} T_\alpha = \varnothing,$$
+ whereas each $T_\alpha$ is non-empty. These are the only properties of the sets $T_\alpha$ used below.
+
+ For $\alpha < \kappa$, define the presheaf $F_\alpha$ on $\C$ on objects by
+ $$F_\alpha(A) \coloneqq T_\alpha, \quad F_\alpha(B) \coloneqq T_\alpha \times T_\alpha, \quad F_\alpha(X) \coloneqq \{\ast\}.$$
+ The maps $u_X^* : F_\alpha(A) \to F_\alpha(X)$ and $v_X^* : F_\alpha(B) \to F_\alpha(X)$ are uniquely determined. The map $f^* : F_\alpha(B) \to F_\alpha(A)$ is the projection $(x,y) \mapsto x$ onto the first coordinate, while the map $g^* : F_\alpha(B) \to F_\alpha(A)$ is the projection $(x,y) \mapsto y$ onto the second coordinate. Since $F_\alpha(X)$ is a singleton, $F_\alpha$ is clearly a presheaf.
+
+ In fact, it is a small presheaf: By the description of small presheaves, it suffices to prove that the diagram
+ $$T_\alpha \times T_\alpha ~\overset{(x,y) \mapsto x}{\underset{(x,y) \mapsto y}{\rightrightarrows}}~ T_\alpha \xrightarrow{!} \{\ast\}.$$
+ is a coequalizer diagram. This is clear since $T_\alpha$ is non-empty.
+
+ For $\beta \leq \alpha$, define the morphism $F_\alpha \to F_\beta$ using the inclusion $T_\alpha \to T_\beta$ at $A$, its product with itself at $B$, and the unique map at $X$. Naturality is immediate.
+
+ The presheaf limit $L \coloneqq \lim_\alpha F_\alpha$ takes $A$ and $B$ to $\varnothing$, since $\lim_\alpha T_\alpha = \varnothing$, while it takes each set $X$ to $\{\ast\}$. As we have seen in previous proofs, $L$ is not small, since for every set $X$ the map $u_X^* : L(A) \to L(X)$ is not surjective.
+
+ - property: equalizers of cokernel pairs
+ proof: >-
+ Consider the morphism of small presheaves
+ $$(f_*;g_*) : \Hom(-,A) \sqcup \Hom(-,A) \to \Hom(-,B).$$
+ We claim that its cokernel pair has no equalizer. By Lemma 4 here, this equalizer must be the objectwise defined equalizer $E$ in the category of presheaves. Since the equalizer of the cokernel pair of a map of sets is equal to its image, we see that, for every object $O \in \C$, the set $E(O)$ is the image of the map
+ $$(f_*;g_*) : \Hom(O,A) \sqcup \Hom(O,A) \to \Hom(O,B).$$
+ Therefore, $E(B) = \varnothing$, $E(A) = \{f,g\}$, and $E(X) = \{v_X\}$ for every set $X$.
+
+ We now use the description of small presheaves to prove that $E$ is not small. It suffices to prove that for every set $X$ the diagram
+ $$\varnothing ~\overset{f^*}{\underset{g^*}{\rightrightarrows}}~ \{f,g\} \xrightarrow{u_X^*} \{v_X\}.$$
+ is not a coequalizer diagram. This is clear since $f^*=g^*$, so the coequalizer of $f^*,g^*$ is just $\{f,g\}$.
+
+ # We can keep this proof here because at some point we will drop
+ # the assumption of cofiltered limits for this property to hold,
+ # and then this proof will not be redundant anymore.
+ # - property: cofiltered-limit-stable epimorphisms
+ # references:
+ # - terminal_presheaf_small
+ # proof: We already know that the terminal presheaf $1$ is small. Now consider for $n \in \IN$ the copower $\IN_{\geq n} \otimes 1$ and for $n < m$ the morphism $\IN_{\geq m} \otimes 1 \to \IN_{\geq n} \otimes 1$ induced by the inclusion $\IN_{\geq m} \subseteq \IN_{\geq n}$. This sequence has a limit, the empty presheaf; this can easily be deduced from $\bigcap_{n \in \IN} \IN_{\geq n} = \varnothing$ in $\IN$. Therefore, the unique morphisms $\IN_{\geq n} \otimes 1 \to 1$ are epimorphisms, but their limit $0 \to 1$ is not.
+
+ - property: generating set
+ proof: Assume that a generating set exists. By writing each presheaf in that generating set as a small colimit of representable functors, we find a set of sets $\S$ such that the representable functors $\Hom(-,A)$, $\Hom(-,B)$ and the $\Hom(-,X)$ for $X \in \S$ provide a generating set. (It is possible that $\Hom(-,A)$ and/or $\Hom(-,B)$ are not required, but it does not hurt to add them.) Let $Y$ be any set that is not contained in $\S$; it surely exists. There are two evident endomorphisms of the small presheaf $\Hom(-,Y) + \Hom(-,Y)$, the identity and the flip. They are not equal since $\Hom(Y,Y) = \{\id_Y\}$ is not empty. Thus, there is a morphism from one of the mentioned representable functors that distinguishes them. But actually, there is no morphism $\Hom(-,A) \to \Hom(-,Y) + \Hom(-,Y)$ at all since there is no morphism $A \to Y$, and likewise there is no morphism from $\Hom(-,B)$, and also not from $\Hom(-,X)$ for $X \in \S$ since $X \neq Y$.
+
+ - property: cogenerator
+ proof: >-
+ Assume that a cogenerator $Q$ exists. For every set $X$, consider the equivalence relation $\ker(u_X^* : Q(A) \to Q(X))$ on $Q(A)$. Since $Q(A)$ is a set, while there is a proper collection of sets, there are distinct sets $X,Y$ that induce the same equivalence relation:
+ $$\ker(u_X^*) = \ker(u_Y^*).$$
+ Using the morphism $u_X : X \to A$, consider the small presheaf
+ $$P \coloneqq \Hom(-,A) \sqcup_{\Hom(-,X)} \Hom(-,A).$$
+ Denote the two inclusions $\Hom(-,A) \to P$ by $i_1$ and $i_2$. For almost every object $O \in \C$, the canonical map $\Hom(O,A) \sqcup \Hom(O,A) \to P(O)$ is bijective; the only exception is $O = X$, for which $P(X)$ consists of the single element $i_1(u_X) = i_2(u_X)$. In particular, $P(A)$ consists of the two elements $i_1(\id_A)$ and $i_2(\id_A)$, while $P(Y)$ consists of the two elements $i_1(u_Y)$ and $i_2(u_Y)$. By the Yoneda Lemma, these correspond to two morphisms
+ $$\alpha_1,\alpha_2 : \Hom(-,Y) \rightrightarrows P.$$
+ We claim that $\gamma \circ \alpha_1 = \gamma \circ \alpha_2$ for every morphism $\gamma : P \to Q$, showing that $Q$ is not a cogenerator.
+
+ Consider the two elements $q_1 \coloneqq \gamma_A(i_1(\id_A))$ and $q_2 \coloneqq \gamma_A(i_2(\id_A))$ of $Q(A)$. They have the same image under $u_X^* : Q(A) \to Q(X)$ because, by construction of $P$, the elements $i_1(\id_A)$ and $i_2(\id_A)$ of $P(A)$ have the same image under $u_X^* : P(A) \to P(X)$. Hence, $\ker(u_X^*) = \ker(u_Y^*)$ implies that $q_1$ and $q_2$ have the same image under $u_Y^*$. Thus,
+ $$\gamma_Y(i_1(u_Y)) = u_Y^*(q_1) = u_Y^*(q_2) = \gamma_Y(i_2(u_Y)).$$
+ By the Yoneda Lemma, this is equivalent to $\gamma \circ \alpha_1 = \gamma \circ \alpha_2$.
+
+special_objects:
+ initial object:
+ description: constant presheaf with value $0$
+ terminal object:
+ description: constant presheaf with value $1$
+ coproducts:
+ description: objectwise defined disjoint union of presheaves
+
+special_morphisms:
+ isomorphisms:
+ description: natural isomorphisms
+ proof: This is trivial.
+ monomorphisms:
+ description: natural transformations that are injective at every object
+ proof: See Lemma 5 here.
+ epimorphisms:
+ description: natural transformations that are surjective at every object
+ proof: See Lemma 5 here.
diff --git a/database/data/macros.yaml b/database/data/macros.yaml
index 3f7829fd..f1f32856 100644
--- a/database/data/macros.yaml
+++ b/database/data/macros.yaml
@@ -48,6 +48,7 @@
\Bilin: \operatorname{Bilin}
\Ob: \operatorname{Ob}
\id: \operatorname{id}
+\ev: \operatorname{ev}
\card: \operatorname{card}
\colim: \operatorname{colim}
\im: \operatorname{im}