Two properties of the category of uniform spaces remain open after #312: if it is regular or coregular. Probably the category is coregular (but not regular). The proof of coregularity cannot be the same as for Top and Meas since the uniform structure on a quotient is not as easy. Gemini has produced the following proof that Unif is coregular. This needs to be checked and then added to the database if it is correct. I will paste the proof here so that it doesn't get lost. Warning. AI can (and will) make errors.
The underlying set of the pushout in $\mathbf{Unif}$ is just the pushout in $\mathbf{Set}$, and the complexity lies entirely in the entourages. Because the composition axiom requires a sequence of entourages satisfying $W_{n+1} \circ W_{n+1} \subseteq W_n$, we cannot just map a single entourage forward. We have to close it under finite chains.
We can prove this stability entirely relationally—without ever defining a real-valued pseudometric—by using a combinatorial "word length" rule on sequences of entourages.
Here is the direct proof.
1. The Setup
Let $i: A \to B$ be a regular mono (uniform embedding) and $f: A \to C$ be any uniformly continuous map. Let $P = B \sqcup_A C$ be the pushout in $\mathbf{Set}$, with canonical maps $g: B \to P$ and $j: C \to P$.
We need to show that $j: C \to P$ is a uniform embedding.
-
Injectivity: Because $i$ is injective, pushout properties in $\mathbf{Set}$ guarantee that $j$ is injective.
-
Uniformity: We need to show that the subspace uniformity induced on $C$ by $P$ is exactly the original uniformity on $C$. Since $j$ is uniformly continuous, we only need to prove that for every entourage $U \in E_C$, there is an entourage $W \in E_P$ such that $(j \times j)^{-1}(W) \subseteq U$.
2. Matching the Sequences
Let $U \in E_C$ be given. We first construct the sequence you mentioned on $C$: choose a sequence of symmetric entourages $U_n \in E_C$ such that $U_0 = U$ and $U_{n+1} \circ U_{n+1} \subseteq U_n$ for all $n \ge 0$.
Because $f$ is uniformly continuous, the preimage $(f \times f)^{-1}(U_n)$ is an entourage on $A$.
Because $i: A \to B$ is a uniform embedding, its pullbacks generate the exact uniformity on $A$. Therefore, for each $n$, there exists a symmetric entourage $V_n \in E_B$ such that:
$$(i \times i)^{-1}(V_n) \subseteq (f \times f)^{-1}(U_n)$$
By standard uniform space operations, we can recursively shrink the $V_n$ sequence to also guarantee the composition rule $V_{n+1} \circ V_{n+1} \subseteq V_n$ on $B$.
3. Constructing Pushout Entourages Combinatorially
Now we build the entourages on $P$. Let $Q_n$ be the raw, uncomposed image of the $n$-th entourages:
$$Q_n = (j \times j)(U_n) \cup (g \times g)(V_n) \cup \Delta_P$$
Because $Q_{n+1} \circ Q_{n+1}$ is not necessarily contained in $Q_n$ (one might step from $C$ to $B$ across the glued subspace $A$), we define $W_n \subseteq P \times P$ by taking the closure over "admissible" finite chains.
We say a chain of points $z_0, z_1, \dots, z_k$ in $P$ is $n$-admissible if each step $(z_{l-1}, z_l) \in Q_{m_l}$ for some index $m_l$, and the indices satisfy the dyadic weight condition:
$$\sum_{l=1}^k 2^{-m_l} \le 2^{-n}$$
(Note: We are using fractions purely as a combinatorial rule for concatenating relations, completely avoiding metric functions on the spaces).
Let $W_n$ be the set of all pairs $(x, y) \in P \times P$ connected by an $n$-admissible chain.
This sequence immediately satisfies $W_{n+1} \circ W_{n+1} \subseteq W_n$ (since concatenating an $(n+1)$-admissible chain with another $(n+1)$-admissible chain yields a sum of weights $\le 2^{-(n+1)} + 2^{-(n+1)} = 2^{-n}$, making it $n$-admissible). Since $W_n$ contains $Q_n$, it pulls back to entourages in $B$ and $C$, meaning $W_n$ are valid entourages for the final uniformity on $P$.
4. The Projection Argument (No Short-Circuiting)
We want to prove that $(j \times j)^{-1}(W_0) \subseteq U_0 = U$.
Suppose $(j(c_1), j(c_2)) \in W_0$. This means there is a $0$-admissible chain in $P$ from $j(c_1)$ to $j(c_2)$. The chain alternates between steps in $j(C)$ and steps in $g(B)$.
Consider any contiguous "excursion" the chain makes into $g(B \setminus A)$. Such an excursion must start and end at the boundary where $B$ and $C$ meet—which is exactly the image of $A$.
Therefore, a $B$-excursion looks like a sequence of points in $g(B)$ starting at some $g(i(a_p)) = j(f(a_p))$ and ending at $g(i(a_q)) = j(f(a_q))$, taking steps entirely in $V_{m_l}$.
Let the sum of the weights $2^{-m_l}$ of this specific $B$-excursion be bounded by $2^{-M}$ for some integer $M$.
By the standard relational chaining lemma (which holds because $V_{k+1} \circ V_{k+1} \subseteq V_k$), this sequence of steps in $B$ composes to a single pair in $V_M$:
$$(i(a_p), i(a_q)) \in V_M$$
Here is the magic step: By our earlier choice of $V_M$, the fact that $(i(a_p), i(a_q)) \in V_M$ implies that:
$$(a_p, a_q) \in (i \times i)^{-1}(V_M) \subseteq (f \times f)^{-1}(U_M)$$
Which means:
$$(f(a_p), f(a_q)) \in U_M$$
This tells us that any excursion into the glued space $B$ can be canonically replaced by a single step in $C$ using $U_M$, and this replacement has a weight $2^{-M}$ which is less than or equal to the sum of the weights of the $B$-steps it replaced.
5. Conclusion
By applying this projection to every $B$-excursion, our original $0$-admissible chain from $j(c_1)$ to $j(c_2)$ in $P$ collapses into a chain lying entirely in $C$, taking steps only in $U$-entourages.
Crucially, because the weights of the replaced steps only decreased or stayed the same, the new $C$-chain is still $0$-admissible! By applying the relational chaining lemma one last time to $C$ (using $U_{n+1} \circ U_{n+1} \subseteq U_n$), the entire $C$-chain composes into $U_0$.
Thus, $(c_1, c_2) \in U_0 = U$. We have successfully shown that $(j \times j)^{-1}(W_0) \subseteq U$, proving that $j$ is a uniform embedding. Regular monos are stable under pushouts, and $\mathbf{Unif}$ is a coregular category.
Two properties of the category of uniform spaces remain open after #312: if it is regular or coregular. Probably the category is coregular (but not regular). The proof of coregularity cannot be the same as for Top and Meas since the uniform structure on a quotient is not as easy. Gemini has produced the following proof that Unif is coregular. This needs to be checked and then added to the database if it is correct. I will paste the proof here so that it doesn't get lost. Warning. AI can (and will) make errors.
The underlying set of the pushout in$\mathbf{Unif}$ is just the pushout in $\mathbf{Set}$ , and the complexity lies entirely in the entourages. Because the composition axiom requires a sequence of entourages satisfying $W_{n+1} \circ W_{n+1} \subseteq W_n$ , we cannot just map a single entourage forward. We have to close it under finite chains.
We can prove this stability entirely relationally—without ever defining a real-valued pseudometric—by using a combinatorial "word length" rule on sequences of entourages.
Here is the direct proof.
1. The Setup
Let$i: A \to B$ be a regular mono (uniform embedding) and $f: A \to C$ be any uniformly continuous map. Let $P = B \sqcup_A C$ be the pushout in $\mathbf{Set}$ , with canonical maps $g: B \to P$ and $j: C \to P$ .
We need to show that$j: C \to P$ is a uniform embedding.
2. Matching the Sequences
Let$U \in E_C$ be given. We first construct the sequence you mentioned on $C$ : choose a sequence of symmetric entourages $U_n \in E_C$ such that $U_0 = U$ and $U_{n+1} \circ U_{n+1} \subseteq U_n$ for all $n \ge 0$ .
Because$f$ is uniformly continuous, the preimage $(f \times f)^{-1}(U_n)$ is an entourage on $A$ .$i: A \to B$ is a uniform embedding, its pullbacks generate the exact uniformity on $A$ . Therefore, for each $n$ , there exists a symmetric entourage $V_n \in E_B$ such that:
Because
By standard uniform space operations, we can recursively shrink the$V_n$ sequence to also guarantee the composition rule $V_{n+1} \circ V_{n+1} \subseteq V_n$ on $B$ .
3. Constructing Pushout Entourages Combinatorially
Now we build the entourages on$P$ . Let $Q_n$ be the raw, uncomposed image of the $n$ -th entourages:
Because$Q_{n+1} \circ Q_{n+1}$ is not necessarily contained in $Q_n$ (one might step from $C$ to $B$ across the glued subspace $A$ ), we define $W_n \subseteq P \times P$ by taking the closure over "admissible" finite chains.
We say a chain of points$z_0, z_1, \dots, z_k$ in $P$ is $n$ -admissible if each step $(z_{l-1}, z_l) \in Q_{m_l}$ for some index $m_l$ , and the indices satisfy the dyadic weight condition:
(Note: We are using fractions purely as a combinatorial rule for concatenating relations, completely avoiding metric functions on the spaces).
Let$W_n$ be the set of all pairs $(x, y) \in P \times P$ connected by an $n$ -admissible chain.$W_{n+1} \circ W_{n+1} \subseteq W_n$ (since concatenating an $(n+1)$ -admissible chain with another $(n+1)$ -admissible chain yields a sum of weights $\le 2^{-(n+1)} + 2^{-(n+1)} = 2^{-n}$ , making it $n$ -admissible). Since $W_n$ contains $Q_n$ , it pulls back to entourages in $B$ and $C$ , meaning $W_n$ are valid entourages for the final uniformity on $P$ .
This sequence immediately satisfies
4. The Projection Argument (No Short-Circuiting)
We want to prove that$(j \times j)^{-1}(W_0) \subseteq U_0 = U$ .
Suppose$(j(c_1), j(c_2)) \in W_0$ . This means there is a $0$ -admissible chain in $P$ from $j(c_1)$ to $j(c_2)$ . The chain alternates between steps in $j(C)$ and steps in $g(B)$ .
Consider any contiguous "excursion" the chain makes into$g(B \setminus A)$ . Such an excursion must start and end at the boundary where $B$ and $C$ meet—which is exactly the image of $A$ .$B$ -excursion looks like a sequence of points in $g(B)$ starting at some $g(i(a_p)) = j(f(a_p))$ and ending at $g(i(a_q)) = j(f(a_q))$ , taking steps entirely in $V_{m_l}$ .
Therefore, a
Let the sum of the weights$2^{-m_l}$ of this specific $B$ -excursion be bounded by $2^{-M}$ for some integer $M$ .$V_{k+1} \circ V_{k+1} \subseteq V_k$ ), this sequence of steps in $B$ composes to a single pair in $V_M$ :
By the standard relational chaining lemma (which holds because
Here is the magic step: By our earlier choice of$V_M$ , the fact that $(i(a_p), i(a_q)) \in V_M$ implies that:
Which means:
This tells us that any excursion into the glued space$B$ can be canonically replaced by a single step in $C$ using $U_M$ , and this replacement has a weight $2^{-M}$ which is less than or equal to the sum of the weights of the $B$ -steps it replaced.
5. Conclusion
By applying this projection to every$B$ -excursion, our original $0$ -admissible chain from $j(c_1)$ to $j(c_2)$ in $P$ collapses into a chain lying entirely in $C$ , taking steps only in $U$ -entourages.
Crucially, because the weights of the replaced steps only decreased or stayed the same, the new$C$ -chain is still $0$ -admissible! By applying the relational chaining lemma one last time to $C$ (using $U_{n+1} \circ U_{n+1} \subseteq U_n$ ), the entire $C$ -chain composes into $U_0$ .
Thus,$(c_1, c_2) \in U_0 = U$ . We have successfully shown that $(j \times j)^{-1}(W_0) \subseteq U$ , proving that $j$ is a uniform embedding. Regular monos are stable under pushouts, and $\mathbf{Unif}$ is a coregular category.