A 2-category is called regular if
In particular, the last condition implies that every 2-congruence which is a kernel has a quotient.
Cat 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 be a finitely complete 2-category where esos are stable under pullback, let be eso, and let be a map. 1. If the induced morphism is ff, then is faithful. 1. If is an equivalence, then is ff.
First note that being ff means that if and are such that , then . Likewise, being an equivalence means that given any , there exists a unique such that .
We first show that is faithful under the first hypothesis. Suppose we have and with . Take the pullback
Then we have two 2-cells
such that the composites
are equal. By the hypothesis, implies . But is eso, since it is a pullback of the eso , so this implies . Thus, is faithful.
Now suppose the (stronger) second hypothesis, and form the pair of pullbacks:
Then , being a pullback of , is eso. We also have a commutative square
By assumption, is an equivalence. Since we have shown that is faithful, the bottom map is ff, so since the eso factors through it, it must be an equivalence as well. But this says precisely that 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 factors as where is ff and is eso, and 1. every eso is the quotient of its kernel.
First suppose is regular; we must show the last two conditions. Let be any morphism. By assumption, the kernel can be completed to an exact 2-fork . Since is the quotient of the 2-congruence , it is eso, and since comes with an action by , we have an induced map with . But since the 2-fork is exact, we also have , so by Street’s Lemma, is ff.
Now suppose that in the previous paragraph were already eso. Then since it factors through the ff , must be an equivalence; thus is equivalent to and hence is a quotient of its kernel.
Now suppose satisfies the conditions in the lemma. Let be any morphism; we must show that can be completed to an exact 2-fork. Factor where is ff and is eso. Since is ff, we have . But every eso is the quotient of its kernel, so the fork is exact.
In a regular 2-category , we call a ff with codomain a subobject of . We write for the preorder of subobjects of , as a full sub-2-category of the slice 2-category . Since is finitely complete and pullbacks preserve ffs, we have pullback functors for any .
If where is ff and is eso, we call the image of . Taking images defines a left adjoint to 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 is regular, so are:
The slice 2-category does not, in general, inherit regularity, but we have:
If is regular, so are the fibrational slices and .
The above definitions and observations are originally due to