In Cat and Gpd, in addition to the (eso, ff) factorization system that is enshrined in the notion of regular 2-category, there is also an (eso+full, faithful) factorization system. In Gpd, the (eso+full, faithful) factorization is the same as the comprehensive factorization, but in Cat they are different.
Mathieu Dupont has pointed out that given sufficient exactness, (eso+full, faithful) factorizations can be constructed from (eso,ff) factorizations. Here we give the argument.
Recall that a morphism is said to be faithful if is faithful for any .
A morphism in a 2-category is eso+full if for any faithful , the following square is a pullback:
A morphism is said to be full if we have where is ff and is eso+full.
Luckily, the terminology is consistent:
In any 2-category, 1. is eso+full if and only if it is both eso and full. 1. is ff if and only if it is both faithful and full.
Since ffs are faithful, any eso+full is eso, and any eso+full clearly factors as an eso+full (itself) followed by an ff (the identity). Conversely, if is eso and where is eso+full and is ff, then is an equivalence, and hence , like , is eso+full.
Now, ffs are clearly faithful, and any ff clearly factors as an eso+full (the identity) followed by an ff (itself). Conversely, if is faithful and we have where is eso+full and is ff, then is also faithful, and hence an equivalence; thus , like , is ff.
Any eso+full morphism is co-ff.
Let be eso+full; we want to show that is ff. It is faithful since is eso, so suppose that and that ; we want to show for some . Let with be the inserter of . Then we have a such that and (modulo this isomorphism) . But since , being an inserter, is faithful, and is eso+full, we have with and therefore ; thus is our desired 2-cell.
If is a 2-congruence such that is eso, then its quotient (if it has one) is eso+full.
Suppose that is faithful and that ; we want to show there is a with and (the rest follows by standard arguments). Since comes with an action by , it suffices to lift this action to itself, and since is faithful it suffices to lift the 2-cell defining the action. This follows by the existence of a diagonal lift in the following rectangle:
which exists since is eso (by assumption) and is ff (since is faithful).
In a regular 2-category, if is a map such that is eso, then is full.
The (eso,ff) factorization of is constructed by taking the quotient of . But by assumption, this kernel has the property of Lemma 3, so the eso part of the (eso,ff) factorization of is eso+full. Hence is full, by definition.
For comparison, recall that
I do not know whether the converse of Lemma 4 is true in general, but it is at least true in an exact 2-category.
Let be an -exact -category, where is 2, (2,1), (1,2), or 1. Then: 1. Every morphism factors as where is eso+full and is faithful. Thus, (eso+full, faithful) is a factorization system on . 1. A morphism is full iff is eso. 1. Therefore, is eso+full iff it is the quotient of a 2-congruence such that is eso.
Of course, the cases and are fairly trivial, since in those cases every morphism in an -category is faithful and thus the only eso+full morphisms are the equivalences. However, we include them for completeness.
For the first statement, let be any morphism, and factor as an eso followed by a ff to get . Then inherits the structure of a 2-congruence, which is an -congruence since is. Since is -exact, this -congruence has a quotient , which is eso+full by Lemma 3, and clearly factors through as . Finally, since is ff by definition, Street's Lemma implies that is faithful.
The “if” direction of the second statement is Lemma 4. Conversely, if where is ff and is eso+full, then must be obtained, up to equivalence, as the quotient of the -congruence constructed above, for which is eso. But since is ff, we have , so is eso as desired.
One direction of the third statement is Lemma 3. For the other, if is eso+full, then by the second statement is eso, and because is eso it is the quotient of its kernel, namely .
Inspecting the proof shows that we don’t need the full strength of exactness, either; all we need is that any sub-congruence of a kernel has a quotient. This is a property in between regularity and exactness. For instance, it is satisfied by , which is not exact.
In a (2,1)-exact (2,1)-category, eso+full morphisms are stable under pullback, and therefore so are full ones.
If is eso+full, then it is the quotient of its kernel, which in a (2,1)-category is . And since is eso+full, by Theorem 1, is eso. If
is a pullback square, then the kernel is also the pullback of along . Thus, by properties of pullback squares, is a pullback of , and hence also eso. But , being eso (as a pullback of ), is also the quotient of its kernel, so by Lemma 3 is eso+full. The second statement follows since ffs are certainly stable under pullback.
Let be an -exact -category. Then: 1. Full morphisms are stable under composition. 1. A morphism is full iff it is (isomorphic to) a composite of eso+full and ff morphisms. 1. If is full and is eso, then is full.
Given and , we have two pullback squares
Thus, if and are full, so that and are eso, then is also eso, hence so is ; thus is full. This proves the first statement, from which the second follows. For the third, if is full and is eso, then is eso, and so is since it is a pullback of . Thus the composite is eso, and since it factors through , it follows that is also eso; hence is full.