2-natural transformation?
The notion of regular 2-catory is the analog in 2-category theory of the notion of regular category in category theory.
A 2-category $K$ is called regular if
esos are stable under 2-pullback;
Every 2-congruence which is a kernel can be completed to an exact 2-fork.
In particular, the last condition implies that every 2-congruence which is a kernel has a quotient.
Cat is regular.
A 1-category is regular as a 2-category iff it is regular as a 1-category, since the esos in a 1-category are precisely the strong epis.
Every finitely complete] (0,1)-category (that is, every meet-semilattice) is regular.
In StreetCBS the last condition is replaced by
We now show that this follows from our definition. First we need:
(Street’s Lemma) Let $K$ be a finitely complete 2-category where esos are stable under pullback, let $e:A\to B$ be eso, and let $n:B\to C$ be a map. 1. If the induced morphism $ker(e) \to ker(n e)$ is ff, then $n$ is faithful. 1. If $ker(e) \to ker(n e)$ is an equivalence, then $n$ is ff.
First note that $ker(e)\to ker(n e)$ being ff means that if $a_1,a_2: Y \rightrightarrows A$ and $\delta_1,\delta_2 : e a_1 \;\rightrightarrows\; e a_2$ are such that $n \delta_1 = n \delta_2$, then $\delta_1=\delta_2$. Likewise, $ker(e)\to ker(n e)$ being an equivalence means that given any $\alpha: n e a_1 \to n e a_2$, there exists a unique $\delta: e a_1 \to e a_2$ such that $n \delta = \alpha$.
We first show that $n$ is faithful under the first hypothesis. Suppose we have $b_1,b_2:X \rightrightarrows B$ and $\beta_1,\beta_2:b_1\to b_2$ with $n \beta_1 = n \beta_2$. Take the pullback
Then we have two 2-cells
such that the composites
are equal. By the hypothesis, $n \beta_1 r = n \beta_2 r$ implies $\beta_1 r = \beta_2 r$. But $r$ is eso, since it is a pullback of the eso $e\times e$, so this implies $\beta_1=\beta_2$. Thus, $n$ is faithful.
Now suppose the (stronger) second hypothesis, and form the pair of pullbacks:
Then $g$, being a pullback of $e\times e$, is eso. We also have a commutative square
By assumption, $(e/e) \to (n e / n e)$ is an equivalence. Since we have shown that $n$ is faithful, the bottom map $B^{\mathbf{2}} \to (n/n)$ is ff, so since the eso $g$ factors through it, it must be an equivalence as well. But this says precisely that $n$ is ff.
A 2-category is regular if and only if 1. it has finite limits, 1. esos are stable under pullback, 1. every morphism $f$ factors as $f\cong m e$ where $m$ is ff and $e$ is eso, and 1. every eso is the quotient of its kernel.
First suppose $K$ is regular; we must show the last two conditions. Let $f:A\to B$ be any morphism. By assumption, the kernel $ker(f)$ can be completed to an exact 2-fork $ker(f) \rightrightarrows A \overset{e}{\to} C$. Since $e$ is the quotient of the 2-congruence $ker(f)$, it is eso, and since $f$ comes with an action by $ker(f)$, we have an induced map $m:C\to B$ with $f\cong m e$. But since the 2-fork is exact, we also have $ker(f)\simeq ker(e)$, so by Street’s Lemma, $m$ is ff.
Now suppose that in the previous paragraph $f$ were already eso. Then since it factors through the ff $m$, $m$ must be an equivalence; thus $f$ is equivalent to $e$ and hence is a quotient of its kernel.
Now suppose $K$ satisfies the conditions in the lemma. Let $f:A\to B$ be any morphism; we must show that $ker(f)$ can be completed to an exact 2-fork. Factor $f = m e$ where $m$ is ff and $e$ is eso. Since $m$ is ff, we have $ker(f)\simeq ker(e)$. But every eso is the quotient of its kernel, so the fork $ker(f) \rightrightarrows A \overset{e} \to C$ is exact.
In StreetCBS it is claimed that the final condition in Theorem 1 follows from the other three, but there is a flaw in the proof.
In a regular 2-category $K$, we call a ff $m:A\to X$ with codomain $X$ a subobject of $X$. We write $Sub(X)$ for the preorder of subobjects of $X$, as a full sub-2-category of the slice 2-category $K/X$. Since $K$ is finitely complete and pullbacks preserve ffs, we have pullback functors $f^*:Sub(Y)\to Sub(X)$ for any $f:X\to Y$.
If $g \cong m e$ where $m$ is ff and $e$ is eso, we call $m$ the image of $g$. Taking images defines a left adjoint $\exists_f:Sub(X)\to Sub(Y)$ to $f^*$ in any regular 2-category, and the Beck-Chevalley condition is satisfied for any pullback square, because esos are stable under pullback.
It is easy to check that if $K$ is regular, so are:
The slice 2-category $K/X$ does not, in general, inherit regularity, but we have:
If $K$ is regular, so are the fibrational slices $Opf(X)$ and $Fib(X)$.
See at 2-congruence the section Regularity.
The above definitions and observations are originally due to