A morphism in a 2-category is called ff and retract-closed or rff if is fully faithful and closed under retracts for all . Explicitly this means that (in addition to being ff) if is a retract of for some , then for some .
A morphism is called Cauchy surjective or cso if it is left orthogonal to all rffs; that is, if
is a pullback whenever is rff.
Since rffs are stable under pullback, is cso if and only if whenever it factors through an rff , then is an equivalence.
Every eso is cso, since every rff is ff. Conversely, in a (2,1)-category, every ff is rff, and thus every cso is eso.
In , the Cauchy surjective functors are those for which every object of is a retract of an object of .
Every equifier or inverter is rff. Therefore, every Cauchy surjective morphism is cofaithful and coconservative. In “Modulated bicategories” by Carboni, Johnson, Street, and Verity it is shown that conversely, every coconservative functor in is Cauchy surjective.
In , (cso,rff) is a factorization system. We now show that the same is true in any regular 2-category.
Given , let be its retractor. This is a 2-categorical finite limit which comes with projections and and 2-cells and such that , and which is universal with these properties.
In any 2-category, if is eso, then is Cauchy surjective.
Suppose that is eso and let be such that and is rff; we want to show is an equivalence. But since is rff and is a retract of , it follows that factors through ; whence is an equivalence since is eso.
Now suppose that is regular, and for any , let be an (eso,ff) factorization of . Since is a retract of , there is a canonical with and .
In a regular 2-category, if is ff and (hence ), then is rff.
Suppose is ff and , and let and be such that is a retract of . Then and for some . Then we have with . But since in , we have a with as well; hence is rff.
In a regular 2-category , 1. Every morphism factors as a Cauchy surjective morphism followed by an rff. 1. Therefore, (cso,rff) is a factorization system on . 1. A morphism is cso if and only if is eso. 1. Likewise, is rff if and only if it is ff and .
Given any , let , , and be as above, and define . Then . Is easy to check that ; thus is eso, so by Lemma 1 is Cauchy surjective.
Now let be the retractor of , with , , and corresponding factorization . Let
be a pullback. Then , like , is eso, and thus so is . Now is a retract of , and is a retract of , so is a retract of . Therefore, is also a retract of , so there is a morphism with (and ). Now in the square
is ff and is eso, so we have in ; thus by Lemma 2 is rff.
Therefore, with we have factored as a cso followed by an rff; this shows the first two statements. Moreover, satisfies the condition of Lemma 1, so if is cso and hence equivalent to , so does it. Likewise, satisfies the condition of Lemma 2, so if is rff and hence equivalent to , so does it.
From the characterization of csos and rffs in Theorem 1, we can conclude that csos and rffs have the expected descriptions in the internal logic.
In a regular 2-category, a morphism is Cauchy surjective if and only if the following sequent is valid in the internal logic:
The context is easily seen to be precisely .
In a regular 2-category, a morphism is rff if and only if it is ff and the following sequent is valid in the internal logic:
The validity of this sequent says that the pullback of along is eso. But since both and factor through the ff , this pullback is equivalent to the pullback of along . Since is eso, this pullback being eso is equivalent to being eso. And since is ff, so is ; thus this is equivalent to being an equivalence.