Next, we show that is a regular category, i.e.:
Recall that a regular epimorphism is a morphism that is the coequalizer of some pair of maps. Thus in 3 the pullback of a coequalizer is required to again be a coequalizer, but not necessarily of the pulled-back pair.
The obvious candidate for the coequalizer of the kernel pair of is the image of , as defined in \autorefsec:image-factorization. Recall that we defined , with functions and defined by
fitting into a diagram:
Recall that a function is called surjective if or equivalently . We have also said that a function between sets is called injective if , or equivalently if each of its fibers is a mere proposition. Since these are the -connected and -truncated maps in the sense of \autorefcha:hlevels, the general theory there implies that above is surjective and is injective, and that this factorization is stable under pullback.
We now identify surjectivity and injectivity with the appropriate category-theoretic notions. First we observe that categorical monomorphisms and epimorphisms have a slightly stronger equivalent formulation.
The equivalence of conditions 1 and 2 is standard category theory. Now consider the function between sets. Condition 1 says that it is injective, while 3 says that its fibers are mere propositions; hence they are equivalent. And 3 implies 4 by taking and recalling that an inhabited mere proposition is contractible. Finally, 4 implies 1 since if , then and both inhabit the type in 4, hence are equal and so . ∎
A function between sets is injective if and only if it is a monomorphism in .
Left to the reader. ∎
Of course, an epimorphism is a monomorphism in the opposite category. We now show that in , the epimorphisms are precisely the surjections, and also precisely the coequalizers (regular epimorphisms).
The coequalizer of a pair of maps in is defined as the 0-truncation of a general (homotopy) coequalizer. For clarity, we may call this the set-coequalizer. It is convenient to express its universal property as follows.
Let be functions between sets and . The set-coequalizer has the property that, for any set and any with , the type
For any function between sets, the following are equivalent:
is an epimorphism.
Consider the pushout diagram
in defining the mapping cone. Then the type is contractible.
Let be a function between sets, and suppose it to be an epimorphism; we show is contractible. The constructor of gives us an element . We have to show that
Note that is a mere proposition, hence we can use induction on . Of course when is we have , so it suffices to find
where and are the other constructors of . Note that is a homotopy from to , so we find the elements
By the dual of \autorefthm:mono4 (and function extensionality), there is a path
Hence, we may define . We also have
This transport involves precomposition with , which commutes with . Thus, from transport in path types we obtain for any , which gives us .
To complete the construction of , it remains to give a path for all . However, is inhabited by . Since it is a mere proposition, this means it is contractible — and thus equivalent, hence equal, to . This completes the definition of . Now, since is assumed to be contractible, it follows that is equivalent to for any . In particular, is equivalent to for each , and hence contractible. Thus, is surjective.
Finally, suppose to be surjective, and consider a set and two functions with the property that . Since is assumed to be surjective, for all the type is contractible. Thus we have the following equivalences:
using on the second line the fact that is a mere proposition, since is a set. But by assumption, there is an element of the latter type. ∎
The category is regular. Moreover, surjective functions between sets are regular epimorphisms.
It is a standard lemma in category theory that a category is regular as soon as it admits finite limits and a pullback-stable orthogonal factorization system with the monomorphisms, in which case consists automatically of the regular epimorphisms. (See e.g. [elephant, A1.3.4].) The existence of the factorization system was proved in \autorefthm:orth-fact. ∎
Pullbacks of regular epis in are regular epis.
We showed in \autorefthm:stable-images that pullbacks of -connected functions are -connected. By \autoreflem:images_are_coequalizers, it suffices to apply this when . ∎
One of the consequences of being a regular category is that we have an “image” operation on subsets. That is, given , any subset (i.e. a predicate ) has an image which is a subset of . This can be defined directly as , or indirectly as the image (in the previous sense) of the composite function
We will also sometimes use the common notation for the image of .