A 2-category is called coherent if
Here a family $\{{f}_{i}:{A}_{i}\to B\}$ is said to be jointly-eso if whenever $m:C\to B$ is ff and every ${f}_{i}$ factors through $m$ (up to isomorphism), then $m$ is an equivalence.
Likewise, we have infinitary coherent 2-categories in which “finite” in the second two conditions is replaced by “small.”
$\mathrm{Cat}$ is coherent.
A 1-category is coherent as a 2-category iff it is coherent as a 1-category.
A (0,1)-category (= poset) is coherent iff it is a distributive lattice, and infinitary-coherent iff it is a frame.
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 $\{{e}_{i}:{A}_{i}\to B\}$ is finite and jointly-eso and $n:B\to C$ is such that the induced functor $\mathrm{ker}({e}_{i})\to \mathrm{ker}(n{e}_{i})$ is an equivalence, then $n$ 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 $\mathrm{Sub}(X)$ have finite (resp. small) unions that are preserved by pullback.
A coherent 2-category has a strict initial object; that is an initial object $0$ such that any morphism $X\to 0$ is an equivalence.
The empty 2-congruence is the kernel of the empty family (over any object), so it must have a quotient $0$, which is clearly an initial object. The empty family over $0$ is jointly-eso, so for any $X\to 0$ the empty family over $X$ is also jointly-eso; but this clearly makes $X$ initial as well.
Two ffs $m:A\to X$ and $n:B\to X$ are said to be disjoint if the comma objects $(m/n)$ and $(n/m)$ are initial objects. If initial objects are strict, then this implies that the pullback $A{\times}_{X}B$ is also initial, but it is strictly stronger already in $\mathrm{Pos}$.
In a coherent 2-category, if $A\to X$ and $B\to X$ are disjoint subobjects, then their union $A\cup B$ in $\mathrm{Sub}(X)$ is also their coproduct $A+B$.
If $A$ and $B$ are disjoint subobjects of $X$, then the kernel of $\{A\to X,B\to X\}$ is the disjoint union of $\mathrm{ker}(A)$ and $\mathrm{ker}(B)$. Therefore, a quotient of it (which is a union of $A$ and $B$ in $\mathrm{Sub}(X)$) will be a coproduct of $A$ and $B$.
A coproduct $A+B$ in a 2-category is disjoint if $A$ and $B$ are disjoint subobjects of $A+B$. 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 $\{{e}_{i}:{A}_{i}\to B\}$ is jointly-eso iff ${\coprod}_{i}{A}_{i}\to B$ is eso; thus regularity and universal coproducts imply that finite jointly-eso families are stable under pullback. And assuming extensivity, any 2-polycongruence $\{{C}_{ij}\}\rightrightarrows \{{C}_{i}\}$ gives rise to an ordinary 2-congruence ${\coprod}_{ij}{C}_{ij}\rightrightarrows {\coprod}_{i}{C}_{i}$. Likewise, 2-polyforks $\{{C}_{ij}\}\rightrightarrows \{{C}_{i}\}\to X$ correspond to 2-forks ${\coprod}_{ij}{C}_{ij}\rightrightarrows {\coprod}_{i}{C}_{i}\to X$, and the property of being a kernel or a quotient is preserved; thus regularity implies coherency.
If $K$ is coherent, then easily so are ${K}^{\mathrm{co}}$, $\mathrm{disc}(K)$, $\mathrm{gpd}(K)$, $\mathrm{pos}(K)$, and $\mathrm{Sub}(1)$. Moreover, we have:
If $K$ is a coherent 2-category, so are the fibrational slices $\mathrm{Opf}(X)$ and $\mathrm{Fib}(X)$ for any $X\in K$.