diff --git a/content/monic-sequential-colimits-via-congruence-quotients.md b/content/monic-sequential-colimits-via-congruence-quotients.md
deleted file mode 100644
index 9305e9fa..00000000
--- a/content/monic-sequential-colimits-via-congruence-quotients.md
+++ /dev/null
@@ -1,14 +0,0 @@
----
-title: Construction of a colimit of a sequence of monomorphisms as a quotient of a congruence
-description: A countably extensive category with quotients of congruences has colimits of sequences of monomorphisms.
-author: Daniel Schepler
----
-
-## Construction of a colimit of a sequence of monomorphisms as a quotient of a congruence
-
-::: Lemma
-Let $\C$ be a countably extensive category with quotients of congruences. Then $\C$ has colimits of sequences of monomorphisms.
-:::
-
-_Proof._
-Suppose we have a sequence $X_1 \hookrightarrow X_2 \hookrightarrow \cdots$ with corresponding monomorphisms $f_{m,n} : X_m \hookrightarrow X_n$ for $m \le n$. Define $Y$ to be the coproduct of all $X_n$. Now for each $m\le n$, define $E_{m,n} \coloneqq X_m$ with two maps $i_m, i_n \circ f_{m,n} : E_{m,n} \rightrightarrows Y$, and similarly for $m \ge n$ define $E_{m,n} \coloneqq X_n$ with two maps $i_m \circ f_{n,m}, i_n : E_{m,n} \rightrightarrows Y$. Then the coproduct of all $E_{m,n}$, with the induced morphisms to $Y$, forms a congruence. Here to prove the maps are jointly monomorphic, and again in proving transitivity, we use extensivity to split the domain of the generalized elements of $\sum_{m,n=1}^\infty E_{m,n}$ so that without loss of generality we may assume each factors through one of the coproduct inclusions. Now a quotient of this congruence must be a colimit of the sequence. $\square$
diff --git a/database/data/categories/Met_c.yaml b/database/data/categories/Met_c.yaml
index 74e9dd02..69df4746 100644
--- a/database/data/categories/Met_c.yaml
+++ b/database/data/categories/Met_c.yaml
@@ -72,8 +72,37 @@ unsatisfied_properties:
- property: ℵ₁-filtered colimits
proof: See MO/511433 for a proof that the diagram $\omega_1 \to \Met_c$, $\alpha \mapsto \IR^\alpha$ does not have a colimit.
+ - property: regular
+ proof: >-
+ We will find a morphism $f : X \to Y$ in $\Met_c$ whose kernel pair has no coequalizer. The idea is to represent the sequential fan $S_\omega$ as such a coequalizer in $\Top$, and generalize the diagonal argument showing that it is not metrizable.
+
+
+ For $n \geq 1$ consider the subspace
+ $$S_n := \{1/k : k \geq 1\} \cup \{0\}$$
+ of $\IR$, so that $\Hom(S_n,Y)$ corresponds to convergent sequences in $Y$. Each $S_n$ has diameter $1$, so we can endow the coproduct space
+ $$X := \textstyle\coprod_n S_n$$
+ with a metric that extends the metric on each $S_n$ and in which points in $S_n$ and $S_m$ for $n \neq m$ have distance $1$. The points of $X$ will be written as $(n,x)$, where $x \in S_n$. If $p_n$ denotes the $n$th prime number, we have $\lim_{k \to \infty} p_n^{-k} = 0$ in $\IR$, so we have a continuous map $S_n \to \IR$ mapping $1/k \mapsto p_n^{-k}$ and $0 \mapsto 0$. Together, these yield a continuous map
+ $$f : X \to \IR, \, (n,0) \mapsto 0, \, (n,1/k) \mapsto p_n^{-k}.$$
+ Let $\pi_1,\pi_2 : E \rightrightarrows X$ be the kernel pair of $f$. Since $p_n^{-k}$ completely determines $n$ and $k$, $E$ consists precisely of the diagonal and all $((n,0),(m,0))$ for $n,m \geq 1$. Thus, the coequalizer of $\pi_1,\pi_2$ in $\Top$ is the quotient of $X$ that identifies all limit points $(n,0)$ for $n \geq 1$; this space is known as the sequential fan $S_\omega$.
+
+
+ Now assume that $\pi_1,\pi_2$ have a coequalizer $q : X \to Q$ in $\Met_c$, i.e. the universal continuous map from $X$ into a metrizable space such that the point
+ $$0_Q := q(n,0) \in Q$$
+ does not depend on the choice of $n$. Since $Q$ is metrizable, there is a countable decreasing neighborhood basis $(B_m)_{m \geq 1}$ of $0_Q \in Q$. Then $U_m := q^{-1}(B_m)$ is an open neighborhood of $(n,0) \in X$ for any $n$, and in particular of $(m,0)$. Hence, $U_m \cap S_m$ contains almost all points of $S_m$. In particular, we may choose a point $x_m \in U_m \cap S_m$ that is isolated in $S_m$.
+
+
+ Define the subset $A := \{x_m : m \geq 1\}$ of $X$ and let $g : X \to \IR$ be its characteristic function, so that $g(a)=1$ for $a \in A$ and $g(x) = 0$ for $x \in X \setminus A$. To show that $g$ is continuous, it suffices to consider each restriction $g|_{S_m} : S_m \to \IR$. This is the characteristic function of the isolated point $x_m \in S_m$, hence continuous.
+
+
+ Since $g(n,0) = 0$ for all $n \geq 1$, there is a unique continuous map $\tilde{g} : Q \to \IR$ satisfying $\tilde{g} \circ q = g$. The points $q(x_m)$ in $Q$ converge to $0_Q$ because for all $k \geq m$ we have $x_k \in U_k$, hence $q(x_k) \in B_k \subseteq B_m$. Since $\tilde{g}$ is continuous, it follows that $\tilde{g}(q(x_m)) = g(x_m) = 1$ converges to $\tilde{g}(0_Q) = \tilde{g}(q(n,0)) = g(n,0) = 0$, which is a contradiction.
+
+
+ Sketch of an alternative proof: Consider the coproduct $X := \coprod_n \IR^n$ in $\Met_c$. The canonical inclusions $\IR^n \to \ell^2$ into the Hilbert space of square-summable sequences yield a continuous map $f : X \to \ell^2$. A coequalizer of the kernel pair of $f$ would be a colimit of the sequence
+ $$\IR \hookrightarrow \IR^2 \hookrightarrow \IR^3 \cdots$$
+ where each map appends a zero coordinate, and we have seen above that this sequential colimit does not exist.
+
- property: quotients of congruences
- proof: If $\Met_c$ had quotients of congruences, then by this lemma it would have sequential colimits of sequences of monomorphisms. This contradicts MO/510316.
+ proof: In the previous proof we have constructed a morphism whose kernel pair does not have a coequalizer, and every kernel pair is a congruence.
special_objects:
initial object: