A morphism in a 2-category is initial if it is left orthogonal to discrete opfibrations. That is, whenever is a discrete opfibration, the following square is a pullback in :
Every morphism in a 1-exact countably-coherent 2-category (in particular, in an -pretopos for ) factors, up to isomorphism, as an initial morphism followed by a discrete opfibration.
By the 2-categorical analogue of a standard theorem about factorization systems in 1-categories, it suffices to show that
The first point is true in any 2-category. For the second, we factor the inclusion as
and observe that both forgetful functors have left adjoints. The left adjoint to is discretization in the 1-exact and countably-coherent 2-category . The left adjoint to constructs the “free opfibration” on a functor , which is given by .
In any 1-exact countably-coherent 2-category, (initial, discrete opfibration) is a (2-categorical) factorization system.
In any 1-exact countably-coherent 2-category, each pullback functor has a left adjoint .
is given by composing with , then factoring into an initial morphism followed by a discrete opfibration.
In a 1-category, every morphism is a discrete opfibration, so the only initial morphisms are isomorphisms. The factorization system (isomorphisms,all morphisms) is well-known.
In a (2,1)-category, the discrete opfibrations are precisely the faithful morphisms. Thus, in this case the comprehensive factorization system coincides with the (eso+full, faithful) factorization system.
The appropriate Beck-Chevalley condition for the adjunctions refers not to pullback squares, but to comma squares. The easiest proof of this fact uses the internal logic. We start with an internal characterization of initial morphisms, analogous to the classical characterization in as the functors for which each comma category , for , is nonempty and connected.
For the rest of this page we make the standing assumption that is a 1-exact and countably-coherent 2-category.
A morphism in is initial iff the following are internally valid:
where for each , expresses “there is a zigzag of length connecting and over .”
Thus, for instance, we have
and so on.
will be initial iff the discrete-opfibration part of its factorization is an equivalence. By construction, this factorization is the discrete reflection of in , which is constructed as the quotient of the equivalence relation generated by (the power taken in ). Therefore, this discrete reflection will be the terminal object iff
It is fairly evident that is eso iff the first displayed sequent holds in . For the second, note that the kernel of in (or equivalently, in ) is just the pullback , since is discrete as an object of . By definition of , this pullback can be computed as the lax limit
and therefore it is precisely the context of the second displayed sequent. Since is the equivalence relation generated by , it is necessarily contained in this kernel, so it suffices to show the converse implication. But is defined as the symmetric transitive closure of the image of , which makes it essentially a countable union of “zigzags” from , and this translates directly into the conclusion of the second sequent.
Initial morphisms in are stable under transfer across comma squares, in the sense that if
is a comma square with initial, then is also initial.
Given the characterization of initial morphisms in Lemma 1, we can simply observe that the usual proof of this fact in takes place entirely in countably-coherent logic.
The adjunctions for discrete opfibrations in satisfy the Beck-Chevalley condition for comma squares. That is, if
is a comma square, then the canonical transformation between functors is an equivalence.
Note that unlike the case for a pullback square, there is no possible “handedness” ambiguity in saying that a comma square satisfies the Beck-Chevalley condition; there is no transformation at all.
The existence of the transformation in the correct direction also depends on the fact that opfibrational slices are functorial at the level of 2-cells. In particular, for a comma square there is no transformation between functors .
Given a discrete opfibration , let be the (initial,discrete-opfibration) factorization of the composite . Now by properties of comma squares and pullbacks, the pasting composite
is also a comma square, and thus so is
where the upper 2-cell is opcartesian for the opfibration , and the map is obtained from the universal property of the pullback square on the bottom. Again, it follows from general properties of pullbacks and comma squares that the top square in this latter diagram is also a comma square. Thus, by Lemma 2, its left-hand morphism is initial. But then the left-hand composite is an (initial, discrete-opfibration) factorization of , and hence it exhibits the desired equivalence .
Passing to 2-cell duals, we obtain:
For a comma square as above, the canonical transformation between functors is an equivalence.