A 2-category is called coherent if
Here a family is said to be jointly-eso if whenever is ff and every factors through (up to isomorphism), then is an equivalence.
Likewise, we have infinitary coherent 2-categories in which “finite” in the second two conditions is replaced by “small.”
A 1-category is coherent as a 2-category iff it is coherent as a 1-category.
The following are proven just like their unary analogues in a regular 2-category.
(Street’s Lemma) In a finitely complete 2-category where finite jointly-eso families are stable under pullback, if is finite and jointly-eso and is such that the induced functor is an equivalence, then is ff.
A 2-category is coherent if and only if
Of course, there are infinitary versions. In particular, we conclude that in a coherent (resp. infinitary-coherent) 2-category, the posets have finite (resp. small) unions that are preserved by pullback.
A coherent 2-category has a strict initial object; that is an initial object such that any morphism is an equivalence.
The empty 2-congruence is the kernel of the empty family (over any object), so it must have a quotient , which is clearly an initial object. The empty family over is jointly-eso, so for any the empty family over is also jointly-eso; but this clearly makes initial as well.
Two ffs and are said to be disjoint if the comma objects and are initial objects. If initial objects are strict, then this implies that the pullback is also initial, but it is strictly stronger already in .
In a coherent 2-category, if and are disjoint subobjects, then their union in is also their coproduct .
If and are disjoint subobjects of , then the kernel of is the disjoint union of and . Therefore, a quotient of it (which is a union of and in ) will be a coproduct of and .
A coproduct in a 2-category is disjoint if and are disjoint subobjects of . We say a coherent 2-category is positive if any two objects have a disjoint coproduct. By Lemma 3, this is equivalent to saying that any two objects can be embedded as disjoint subobjects of some other object. Disjoint coproducts in a coherent 2-category are automatically stable under pullback, so a positive coherent 2-category is necessarily extensive. Conversely, we have:
A regular and extensive 2-category is coherent (and positive).
In the presence of finite coproducts, a family is jointly-eso iff is eso; thus regularity and universal coproducts imply that finite jointly-eso families are stable under pullback. And assuming extensivity, any 2-polycongruence gives rise to an ordinary 2-congruence . Likewise, 2-polyforks correspond to 2-forks , and the property of being a kernel or a quotient is preserved; thus regularity implies coherency.
If is coherent, then easily so are , , , , and . Moreover, we have:
If is a coherent 2-category, so are the fibrational slices and for any .