10.1.2 Images

Next, we show that ๐’ฎโขeโขt is a regular category, i.e.:

  1. 1.

    ๐’ฎโขeโขt is finitely complete.

  2. 2.

    The kernel pair ๐—‰๐—‹1,๐—‰๐—‹2:(โˆ‘(x,y:A)f(x)=f(y))โ†’A of any function f:Aโ†’B has a coequalizerMathworldPlanetmath.

  3. 3.

    PullbacksPlanetmathPlanetmath of regular epimorphisms are again regular epimorphisms.

Recall that a regular epimorphism is a morphismMathworldPlanetmathPlanetmath 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 f:Aโ†’B is the image of f, as defined in \autorefsec:image-factorization. Recall that we defined ๐—‚๐—†(f):โ‰กโˆ‘(b:B)โˆฅ๐–ฟ๐—‚๐–ปf(b)โˆฅ, with functions f~:Aโ†’๐—‚๐—†โข(f) and if:๐—‚๐—†โข(f)โ†’B defined by

f~ :โ‰กฮปa.(f(a),|(a,๐—‹๐–พ๐–ฟ๐—…fโข(a))|)
if :โ‰ก๐—‰๐—‹1

fitting into a diagram:


Recall that a function f:Aโ†’B is called surjectivePlanetmathPlanetmath if โˆ€(b:B).โˆฅ๐–ฟ๐—‚๐–ปf(b)โˆฅ, or equivalently โˆ€(b:B).โˆƒ(a:A).f(a)=b. We have also said that a function f:Aโ†’B between sets is called injectivePlanetmathPlanetmath if โˆ€(a,aโ€ฒ:A).(f(a)=f(aโ€ฒ))โ‡’(a=aโ€ฒ), or equivalently if each of its fibers is a mere proposition. Since these are the (-1)-connectedPlanetmathPlanetmath and (-1)-truncated maps in the sense of \autorefcha:hlevels, the general theory there implies that f~ above is surjective and if 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 monomorphismsMathworldPlanetmathPlanetmathPlanetmathPlanetmath and epimorphismsMathworldPlanetmath have a slightly stronger equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath formulation.

Lemma 10.1.1.

For a morphism f:homAโก(a,b) in a category A, the following are equivalent.

  1. 1.

    f is a monomorphism: for all x:A and g,h:homAโก(x,a), if fโˆ˜g=fโˆ˜h then g=h.

  2. 2.

    (If A has pullbacks) the diagonal map aโ†’aร—ba is an isomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmath.

  3. 3.

    For all x:A and k:homAโก(x,b), the type โˆ‘(h:homA(x,a))(k=fโˆ˜h) is a mere proposition.

  4. 4.

    For all x:A and g:homAโก(x,a), the type โˆ‘(h:homA(x,a))(fโˆ˜g=fโˆ˜h) is contractibleMathworldPlanetmath.


The equivalence of conditionsย 1 andย 2 is standard category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath. Now consider the function (fโˆ˜โ€“):homAโก(x,a)โ†’homAโก(x,b) 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 k:โ‰กfโˆ˜g and recalling that an inhabited mere proposition is contractible. Finally,ย 4 impliesย 1 since if p:fโˆ˜g=fโˆ˜h, then (g,๐—‹๐–พ๐–ฟ๐—…) and (h,p) both inhabit the type inย 4, hence are equal and so g=h. โˆŽ

Lemma 10.1.2.

A function f:Aโ†’B between sets is injective if and only if it is a monomorphism in Sโขeโขt.


Left to the reader. โˆŽ

Of course, an epimorphism is a monomorphism in the opposite category. We now show that in ๐’ฎโขeโขt, the epimorphisms are precisely the surjections, and also precisely the coequalizers (regular epimorphisms).

The coequalizer of a pair of maps f,g:Aโ†’B in ๐’ฎโขeโขt is defined as the 0-truncation of a general (homotopyMathworldPlanetmath) coequalizer. For clarity, we may call this the set-coequalizer. It is convenient to express its universal propertyMathworldPlanetmath as follows.

Lemma 10.1.3.

Let f,g:Aโ†’B be functions between sets A and B. The set-coequalizer cf,g:Bโ†’Q has the property that, for any set C and any h:Bโ†’C with hโˆ˜f=hโˆ˜g, the type


is contractible.

Lemma 10.1.4.

For any function f:Aโ†’B between sets, the following are equivalent:

  1. 1.

    f is an epimorphism.

  2. 2.

    Consider the pushout diagram


    in ๐’ฎโขeโขt defining the mapping cone. Then the type Cf is contractible.

  3. 3.

    f is surjective.


Let f:Aโ†’B be a function between sets, and suppose it to be an epimorphism; we show Cf is contractible. The constructor ๐Ÿโ†’Cf of Cf gives us an element t:Cf. We have to show that


Note that x=t is a mere proposition, hence we can use inductionMathworldPlanetmath on Cf. Of course when x is t we have ๐—‹๐–พ๐–ฟ๐—…t:t=t, so it suffices to find

I0 :โˆb:Bฮนโข(b)=t
I1 :โˆa:Aฮฑ1โข(a)-1โข\centerdotโขI0โข(fโข(a))=๐—‹๐–พ๐–ฟ๐—…t.

where ฮน:Bโ†’Cf and ฮฑ1:โˆ(a:A)ฮนโข(fโข(a))=t are the other constructors of Cf. Note that ฮฑ1 is a homotopy from ฮนโˆ˜f to ๐–ผ๐—ˆ๐—‡๐—Œ๐—tโˆ˜f, so we find the elements


By the dual of \autorefthm:mono4 (and function extensionality), there is a path


Hence, we may define I0(b):โ‰ก๐—๐–บ๐—‰๐—‰๐—…๐—’(๐–บ๐—‰๐—‰๐—‹1(ฮณ),b):ฮน(b)=t. We also have


This transport involves precomposition with f, which commutes with ๐—๐–บ๐—‰๐—‰๐—…๐—’. Thus, from transport in path types we obtain I0โข(fโข(a))=ฮฑ1โข(a) for any a:A, which gives us I1.

Now suppose Cf is contractible; we show f is surjective. We first construct a type family P:Cfโ†’๐–ฏ๐—‹๐—ˆ๐—‰ by recursion on Cf, which is valid since ๐–ฏ๐—‹๐—ˆ๐—‰ is a set. On the point constructors, we define

Pโข(t) :โ‰ก๐Ÿ
Pโข(ฮนโข(b)) :โ‰กโˆฅ๐–ฟ๐—‚๐–ปf(b)โˆฅ.

To completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath the construction of P, it remains to give a path โˆฅ๐–ฟ๐—‚๐–ปf(f(a))โˆฅ=๐–ฏ๐—‹๐—ˆ๐—‰๐Ÿ for all a:A. However, โˆฅ๐–ฟ๐—‚๐–ปfโข(fโข(a))โˆฅ is inhabited by (fโข(a),๐—‹๐–พ๐–ฟ๐—…fโข(a)). Since it is a mere proposition, this means it is contractible โ€” and thus equivalent, hence equal, to ๐Ÿ. This completes the definition of P. Now, since Cf is assumed to be contractible, it follows that Pโข(x) is equivalent to Pโข(t) for any x:Cf. In particular, P(ฮน(b))โ‰กโˆฅ๐–ฟ๐—‚๐–ปf(b)โˆฅ is equivalent to Pโข(t)โ‰ก๐Ÿ for each b:B, and hence contractible. Thus, f is surjective.

Finally, suppose f:Aโ†’B to be surjective, and consider a set C and two functions g,h:Bโ†’C with the property that gโˆ˜f=hโˆ˜f. Since f is assumed to be surjective, for all b:B the type โˆฅ๐–ฟ๐—‚๐–ปfโข(b)โˆฅ is contractible. Thus we have the following equivalences:

โˆb:B(g(b)=h(b)) โ‰ƒโˆb:B(โˆฅ๐–ฟ๐—‚๐–ปf(b)โˆฅโ†’(g(b)=h(b)))

using on the second line the fact that gโข(b)=hโข(b) is a mere proposition, since C is a set. But by assumptionPlanetmathPlanetmath, there is an element of the latter type. โˆŽ

Theorem 10.1.5.

The category Sโขeโขt is regularPlanetmathPlanetmathPlanetmathPlanetmath. 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. โˆŽ

Lemma 10.1.6.

Pullbacks of regular epis in Sโขeโขt are regular epis.


We showed in \autorefthm:stable-images that pullbacks of n-connected functions are n-connected. By \autoreflem:images_are_coequalizers, it suffices to apply this when n=-1. โˆŽ

One of the consequences of ๐’ฎโขeโขt being a regular category is that we have an โ€œimageโ€ operationMathworldPlanetmath on subsets. That is, given f:Aโ†’B, any subset P:๐’ซโข(A) (i.e.ย a predicateMathworldPlanetmath P:Aโ†’๐–ฏ๐—‹๐—ˆ๐—‰) has an image which is a subset of B. This can be defined directly as \setofy:B|โˆƒ(x:A).f(x)=yโˆงP(x), or indirectly as the image (in the previous sense) of the composite function


We will also sometimes use the common notation \setoff(x)|P(x) for the image of P.

Title 10.1.2 Images