10.1.2 Images

Next, we show that $𝒮et$ is a regular category, i.e.:

1. $𝒮et$ is finitely complete.

2. The kernel pair ${\mathrm{𝗉𝗋}}_1,{\mathrm{𝗉𝗋}}_2:({\sum }_{(x,y:A)}f(x)=f(y))\to A$ of anyfunction $f:A\to B$ has a coequalizer.

3. Pullbacks of regular epimorphisms are again regular epimorphisms.

Recall that a regular epimorphismis 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 $f:A\to B$ is the image of $f$, as defined in sec:image-factorization.Recall that we defined $\mathrm{𝗂𝗆}(f):\equiv {\sum }_{(b:B)}\parallel {\mathrm{𝖿𝗂𝖻}}_f(b)\parallel$, with functions$\tilde{f}:A\to \mathrm{𝗂𝗆}(f)$ and $i_f:\mathrm{𝗂𝗆}(f)\to B$ defined by

$\tilde{f}$$:\equiv \lambda a.(f(a),\left|(a,{\mathrm{𝗋𝖾𝖿𝗅}}_{f(a)})\right|)$

$i_f$$:\equiv {\mathrm{𝗉𝗋}}_1$

fitting into a diagram:

Recall that a function $f:A\to B$ is called surjective if$\forall (b:B).\parallel {\mathrm{𝖿𝗂𝖻}}_f(b)\parallel ,$or equivalently $\forall (b:B).\exists (a:A).f(a)=b$.We have also said that a function $f:A\to B$ between sets is called injective if$\forall (a,a^{\prime }:A).(f(a)=f(a^{\prime }))\Rightarrow (a=a^{\prime })$, or equivalently if each of its fibers is a mere proposition.Since these are the $(-1)$-connected and $(-1)$-truncated maps in the sense of cha:hlevels, the general theory there implies that $\tilde{f}$ above is surjective and $i_f$ 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.

Lemma 10.1.1.

For a morphism $f\mathrm{:}{\mathrm{hom}}_A\mathit{}\mathrm{(}a\mathrm{,}b\mathrm{)}$ in a category $A$, the following are equivalent.

1. $f$ is a monomorphism:for all $x:A$ and $g,h:{\mathrm{hom}}_A(x,a)$, if $f\circ g=f\circ h$ then $g=h$.

2. (If $A$ has pullbacks) the diagonal map $a\to a{\times }_{b}a$ is an isomorphism.

3. For all $x:A$ and $k:{\mathrm{hom}}_A(x,b)$, the type ${\sum }_{(h:{\mathrm{hom}}_A(x,a))}(k=f\circ h)$ is a mere proposition.

4. For all $x:A$ and $g:{\mathrm{hom}}_A(x,a)$, the type ${\sum }_{(h:{\mathrm{hom}}_A(x,a))}(f\circ g=f\circ h)$ is contractible.

Proof.

The equivalence of conditions 1 and 2 is standard category theory.Now consider the function $(f\circ \text{–}):{\mathrm{hom}}_A(x,a)\to {\mathrm{hom}}_A(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:\equiv f\circ g$ and recalling that an inhabited mere proposition is contractible.Finally, 4 implies 1 since if $p:f\circ g=f\circ h$, then $(g,\mathrm{𝗋𝖾𝖿𝗅})$ and $(h,p)$ both inhabit the type in 4, hence are equal and so $g=h$.∎

Lemma 10.1.2.

A function $f\mathrm{:}A\mathrm{\to }B$ between sets is injective if and only if it is a monomorphism in $\mathrm{S}\mathit{}e\mathit{}t$.

Proof.

Left to the reader.∎

Of course, an epimorphismis a monomorphism in the opposite category.We now show that in $𝒮et$, the epimorphisms are precisely the surjections, and also precisely the coequalizers (regular epimorphisms).

The coequalizer of a pair of maps $f,g:A\to B$ in $𝒮et$ 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.

Lemma 10.1.3.

Let $f\mathrm{,}g\mathrm{:}A\mathrm{\to }B$ be functions between sets $A$ and $B$. Theset-coequalizer $c_{f\mathrm{,}g}\mathrm{:}B\mathrm{\to }Q$ has the property that, for any set $C$ and any $h\mathrm{:}B\mathrm{\to }C$ with $h\mathrm{\circ }f\mathrm{=}h\mathrm{\circ }g$, the type

$$\sum _{k:Q\to C}(k\circ c_{f,g}=h)$$

is contractible.

Lemma 10.1.4.

For any function $f\mathrm{:}A\mathrm{\to }B$ between sets, the following are equivalent:

1. $f$ is an epimorphism.

2. Consider the pushout diagram

   in $𝒮et$ defining the mapping cone. Then the type $C_f$ is contractible.

3. $f$ is surjective.

Proof.

Let $f:A\to B$ be a function between sets, and suppose it to be an epimorphism; we show $C_f$ is contractible.The constructor $\mathrm{𝟏}\to C_f$ of $C_f$ gives us an element $t:C_f$.We have to show that

$$\prod _{x:C_f}x=t.$$

Note that $x=t$ is a mere proposition, hence we can use induction on $C_f$.Of course when $x$ is $t$ we have ${\mathrm{𝗋𝖾𝖿𝗅}}_t:t=t$, so it suffices to find

$I_0$$:{\displaystyle \prod _{b:B}}\iota (b)=t$

$I_1$$:{\displaystyle \prod _{a:A}}{\alpha }_1{(a)}^{-1}{I}_0(f(a))={\mathrm{𝗋𝖾𝖿𝗅}}_t.$

where $\iota :B\to C_f$ and ${\alpha }_1:{\prod }_{(a:A)}\iota (f(a))=t$ are the other constructorsof $C_f$. Note that ${\alpha }_1$ is a homotopy from $\iota \circ f$ to${\mathrm{𝖼𝗈𝗇𝗌𝗍}}_t\circ f$, so we find the elements

$$(\iota ,{\mathrm{𝗋𝖾𝖿𝗅}}_{\iota \circ f}),({\mathrm{𝖼𝗈𝗇𝗌𝗍}}_t,{\alpha }_1):\sum _{h:B\to C_f}\iota \circ f\sim h\circ f.$$

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

$$\gamma :(\iota ,{\mathrm{𝗋𝖾𝖿𝗅}}_{\iota \circ f})=({\mathrm{𝖼𝗈𝗇𝗌𝗍}}_t,{\alpha }_1).$$

Hence, we may define $I_0(b):\equiv \mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}({\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_1}(\gamma ),b):\iota (b)=t$.We also have

$${\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_2}(\gamma ):{\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_1}{(\gamma )}_{*}\left({\mathrm{𝗋𝖾𝖿𝗅}}_{\iota \circ f}\right)={\alpha }_1.$$

This transport involves precomposition with $f$, which commutes with $\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}$.Thus, from transport in path types we obtain $I_0(f(a))={\alpha }_1(a)$ for any $a:A$, which gives us $I_1$.

Now suppose $C_f$ is contractible; we show $f$ is surjective.We first construct a type family $P:C_f\to \mathrm{𝖯𝗋𝗈𝗉}$ by recursion on $C_f$, which is valid since $\mathrm{𝖯𝗋𝗈𝗉}$ is a set.On the point constructors, we define

$P(t)$$:\equiv \mathrm{𝟏}$

$P(\iota (b))$$:\equiv \parallel {\mathrm{𝖿𝗂𝖻}}_f(b)\parallel .$

To complete the construction of $P$, it remains to give a path$\parallel {\mathrm{𝖿𝗂𝖻}}_f(f(a))\parallel {=}_{\mathrm{𝖯𝗋𝗈𝗉}}\mathrm{𝟏}$for all $a:A$.However, $\parallel {\mathrm{𝖿𝗂𝖻}}_f(f(a))\parallel$ is inhabited by $(f(a),{\mathrm{𝗋𝖾𝖿𝗅}}_{f(a)})$.Since it is a mere proposition, this means it is contractible — and thus equivalent, hence equal, to $\mathrm{𝟏}$.This completes the definition of $P$.Now, since $C_f$ is assumed to be contractible, it follows that $P(x)$ is equivalent to $P(t)$ for any $x:C_f$.In particular, $P(\iota (b))\equiv \parallel {\mathrm{𝖿𝗂𝖻}}_f(b)\parallel$ is equivalent to $P(t)\equiv \mathrm{𝟏}$ for each $b:B$, and hence contractible.Thus, $f$ is surjective.

Finally, suppose $f:A\to B$ to be surjective, and consider a set $C$ and two functions$g,h:B\to C$ with the property that $g\circ f=h\circ f$. Since $f$is assumed to be surjective, for all $b:B$ the type $\parallel {\mathrm{𝖿𝗂𝖻}}_f(b)\parallel$ is contractible.Thus we have the following equivalences:

${\displaystyle \prod _{b:B}}(g(b)=h(b))$$\simeq {\displaystyle \prod _{b:B}}(\parallel {\mathrm{𝖿𝗂𝖻}}_f(b)\parallel \to (g(b)=h(b)))$

$\simeq {\displaystyle \prod _{b:B}}({\mathrm{𝖿𝗂𝖻}}_f(b)\to (g(b)=h(b)))$

$\simeq {\displaystyle \prod _{(b:B)}}{\displaystyle \prod _{(a:A)}}{\displaystyle \prod _{(p:f(a)=b)}}g(b)=h(b)$

$\simeq {\displaystyle \prod _{a:A}}g(f(a))=h(f(a))$

using on the second line the fact that $g(b)=h(b)$ is a mere proposition, since $C$ is a set.But by assumption, there is an element of the latter type.∎

Theorem 10.1.5.

The category $\mathrm{S}\mathit{}e\mathit{}t$ is regular. Moreover, surjective functions between sets are regular epimorphisms.

Proof.

It is a standard lemma in category theory that a category is regular as soon as it admits finite limits and a pullback-stable orthogonalfactorization system $(ℰ,ℳ)$ with $ℳ$ the monomorphisms, in which case $ℰ$ consists automatically ofthe regular epimorphisms.(See e.g. [elephant, A1.3.4].)The existence of the factorization system was proved in thm:orth-fact.∎

Lemma 10.1.6.

Pullbacks of regular epis in $\mathrm{S}\mathit{}e\mathit{}t$ are regular epis.

Proof.

We showed in thm:stable-images that pullbacks of $n$-connected functions are $n$-connected.By lem:images_are_coequalizers, it suffices to apply this when $n=-1$.∎

One of the consequences of $𝒮et$ being a regular category is that we have an “image” operation on subsets.That is, given $f:A\to B$, any subset $P:𝒫(A)$ (i.e. a predicate $P:A\to \mathrm{𝖯𝗋𝗈𝗉}$) has an image which is a subset of $B$.This can be defined directly as $y:B|\exists (x:A).f(x)=y\wedge P(x)$, or indirectly as the image (in the previous sense) of the composite function

$$x:A|P(x)\to A\stackrel{𝑓}{\to }B.$$

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