10.1.2 Images

Next, we show that $\mathcal{S}et$ is a regular category, i.e.:

1.

$\mathcal{S}et$ is finitely complete.
2.

The kernel pair $\mathsf{pr}_{1},\mathsf{pr}_{2}:(\mathchoice{\sum_{x,y:A}\,}{\mathchoice{{% \textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{% \mathchoice{{\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{% (x,y:A)}}}{\mathchoice{{\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:% A)}}{\sum_{(x,y:A)}}}f(x)=f(y))\to A$ of any function $f:A\to B$ has a coequalizer.
3.

Pullbacks of regular epimorphisms are again regular epimorphisms.

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 $f:A\to B$ is the image of $f$ , as defined in \autorefsec:image-factorization. Recall that we defined $\mathsf{im}(f):\!\!\equiv\mathchoice{\sum_{b:B}\,}{\mathchoice{{\textstyle\sum% _{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathchoice{{\textstyle% \sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathchoice{{% \textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}\mathopen{}% \left\|{\mathsf{fib}}_{f}(b)\right\|\mathclose{}$ , with functions $\tilde{f}:A\to\mathsf{im}(f)$ and $i_{f}:\mathsf{im}(f)\to B$ defined by

	$\displaystyle\tilde{f}$	$\displaystyle:\!\!\equiv{\lambda}a.\,{\mathopen{}\left(f(a),\,\mathopen{}\left% \|{\mathopen{}(a,\mathsf{refl}_{f(a)})\mathclose{}}\right\|\mathclose{}\right)% \mathclose{}}$
	$\displaystyle i_{f}$	$\displaystyle:\!\!\equiv\mathsf{pr}_{1}$

fitting into a diagram:

$\xymatrix{**[l]{\mathchoice{\sum_{x,y:A}\,}{\mathchoice{{\textstyle\sum_{(x,y:% A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{\mathchoice{{\textstyle% \sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{\mathchoice{% {\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}f(% x)=f(y)}\ar@<0.25em>[r]^{\mathsf{pr}_{1}}\ar@<-0.25em>[r]_{\mathsf{pr}_{2}}&{A% }\ar[r]^{(}0.4){\tilde{f}}\ar[rd]_{f}&{\mathsf{im}(f)}\ar@{..>}[d]^{i_{f}}\\ &&B}$

Recall that a function $f:A\to B$ is called surjective if $\forall(b:B).\,\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right\|\mathclose{},$ 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 \autorefcha: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:\hom_{A}(a,b)$ in a category $A$ , the following are equivalent.

1.

$f$ is a monomorphism: for all $x : A$ and ${g,h:\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:\hom_{A}(x,b)$ , the type $\mathchoice{\sum_{h:\hom_{A}(x,a)}\,}{\mathchoice{{\textstyle\sum_{(h:\hom_{A}% (x,a))}}}{\sum_{(h:\hom_{A}(x,a))}}{\sum_{(h:\hom_{A}(x,a))}}{\sum_{(h:\hom_{A% }(x,a))}}}{\mathchoice{{\textstyle\sum_{(h:\hom_{A}(x,a))}}}{\sum_{(h:\hom_{A}% (x,a))}}{\sum_{(h:\hom_{A}(x,a))}}{\sum_{(h:\hom_{A}(x,a))}}}{\mathchoice{{% \textstyle\sum_{(h:\hom_{A}(x,a))}}}{\sum_{(h:\hom_{A}(x,a))}}{\sum_{(h:\hom_{% A}(x,a))}}{\sum_{(h:\hom_{A}(x,a))}}}(k=f\circ h)$ is a mere proposition.
4.

For all $x : A$ and ${g:\hom_{A}(x,a)}$ , the type $\mathchoice{\sum_{h:\hom_{A}(x,a)}\,}{\mathchoice{{\textstyle\sum_{(h:\hom_{A}% (x,a))}}}{\sum_{(h:\hom_{A}(x,a))}}{\sum_{(h:\hom_{A}(x,a))}}{\sum_{(h:\hom_{A% }(x,a))}}}{\mathchoice{{\textstyle\sum_{(h:\hom_{A}(x,a))}}}{\sum_{(h:\hom_{A}% (x,a))}}{\sum_{(h:\hom_{A}(x,a))}}{\sum_{(h:\hom_{A}(x,a))}}}{\mathchoice{{% \textstyle\sum_{(h:\hom_{A}(x,a))}}}{\sum_{(h:\hom_{A}(x,a))}}{\sum_{(h:\hom_{% A}(x,a))}}{\sum_{(h:\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\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}):\hom_{A}(x,a)\to\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,\mathsf{refl})$ and $(h,p)$ both inhabit the type in 4, hence are equal and so $g=h$ . ∎

Lemma 10.1.2.

A function $f:A\to B$ between sets is injective if and only if it is a monomorphism in $\mathcal{S}et$ .

Proof.

Left to the reader. ∎

Of course, an epimorphism is a monomorphism in the opposite category. We now show that in $\mathcal{S}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 $\mathcal{S}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,g:A\to B$ be functions between sets $A$ and $B$ . The set-coequalizer $c_{f,g}:B\to Q$ has the property that, for any set $C$ and any $h:B\to C$ with $h\circ f=h\circ g$ , the type

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

is contractible.

Lemma 10.1.4.

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

1.

$f$ is an epimorphism.

Consider the pushout diagram

$\xymatrix{{A}\ar[r]^{f}\ar[d]&{B}\ar[d]^{\iota}\\ {\mathbf{1}}\ar[r]_{t}&{C_{f}}}$

in $\mathcal{S}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 $\mathbf{1}\to C_{f}$ of $C_{f}$ gives us an element $t:C_{f}$ . We have to show that

$\mathchoice{\prod_{x:C_{f}}\,}{\mathchoice{{\textstyle\prod_{(x:C_{f})}}}{% \prod_{(x:C_{f})}}{\prod_{(x:C_{f})}}{\prod_{(x:C_{f})}}}{\mathchoice{{% \textstyle\prod_{(x:C_{f})}}}{\prod_{(x:C_{f})}}{\prod_{(x:C_{f})}}{\prod_{(x:% C_{f})}}}{\mathchoice{{\textstyle\prod_{(x:C_{f})}}}{\prod_{(x:C_{f})}}{\prod_% {(x:C_{f})}}{\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 $\mathsf{refl}_{t}:t=t$ , so it suffices to find

	$\displaystyle I_{0}$	$\displaystyle:\mathchoice{\prod_{b:B}\,}{\mathchoice{{\textstyle\prod_{(b:B)}}% }{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{% (b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle% \prod_{(b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}\iota(b)=t$
	$\displaystyle I_{1}$	$\displaystyle:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}% }{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{% (a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle% \prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\mathord{{\alpha_% {1}(a)}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}% }}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}I_{0}(f(a))=\mathsf{refl}_{t}.$

where $\iota:B\to C_{f}$ and $\alpha_{1}:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle% \prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\iota(f(a))=t$ are the other constructors of $C_{f}$ . Note that $\alpha_{1}$ is a homotopy from $\iota\circ f$ to $\mathsf{const}_{t}\circ f$ , so we find the elements

${\mathopen{}(\iota,\mathsf{refl}_{\iota\circ f})\mathclose{}},{\mathopen{}(% \mathsf{const}_{t},\alpha_{1})\mathclose{}}:\mathchoice{\sum_{h:B\to C_{f}}\,}% {\mathchoice{{\textstyle\sum_{(h:B\to C_{f})}}}{\sum_{(h:B\to C_{f})}}{\sum_{(% h:B\to C_{f})}}{\sum_{(h:B\to C_{f})}}}{\mathchoice{{\textstyle\sum_{(h:B\to C% _{f})}}}{\sum_{(h:B\to C_{f})}}{\sum_{(h:B\to C_{f})}}{\sum_{(h:B\to C_{f})}}}% {\mathchoice{{\textstyle\sum_{(h:B\to C_{f})}}}{\sum_{(h:B\to C_{f})}}{\sum_{(% h:B\to C_{f})}}{\sum_{(h:B\to C_{f})}}}\iota\circ f\sim h\circ f.$

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

$\gamma:{\mathopen{}(\iota,\mathsf{refl}_{\iota\circ f})\mathclose{}}={% \mathopen{}(\mathsf{const}_{t},\alpha_{1})\mathclose{}}.$

Hence, we may define $I_{0}(b):\!\!\equiv\mathsf{happly}(\mathsf{ap}_{\mathsf{pr}_{1}}(\gamma),b):% \iota(b)=t$ . We also have

$\mathsf{ap}_{\mathsf{pr}_{2}}(\gamma):{\mathsf{ap}_{\mathsf{pr}_{1}}(\gamma)}_% {*}\mathopen{}\left({\mathsf{refl}_{\iota\circ f}}\right)\mathclose{}=\alpha_{% 1}.$

This transport involves precomposition with $f$ , which commutes with $\mathsf{happly}$ . 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\mathsf{Prop}$ by recursion on $C_{f}$ , which is valid since $\mathsf{Prop}$ is a set. On the point constructors, we define

	$\displaystyle P(t)$	$\displaystyle:\!\!\equiv\mathbf{1}$
	$\displaystyle P(\iota(b))$	$\displaystyle:\!\!\equiv\mathopen{}\left\\|{\mathsf{fib}}_{f}(b)\right\\|% \mathclose{}.$

To complete the construction of $P$ , it remains to give a path $\mathopen{}\left\|{\mathsf{fib}}_{f}(f(a))\right\|\mathclose{}=_{\mathsf{Prop}% }\mathbf{1}$ for all $a : A$ . However, $\mathopen{}\left\|{\mathsf{fib}}_{f}(f(a))\right\|\mathclose{}$ is inhabited by $(f(a),\mathsf{refl}_{f(a)})$ . Since it is a mere proposition, this means it is contractible — and thus equivalent, hence equal, to $\mathbf{1}$ . 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\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right\|\mathclose{}$ is equivalent to $P(t)\equiv\mathbf{1}$ 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 $\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right\|\mathclose{}$ is contractible. Thus we have the following equivalences:

	$\displaystyle\mathchoice{\prod_{b:B}\,}{\mathchoice{{\textstyle\prod_{(b:B)}}}% {\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{(% b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle% \prod_{(b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}(g(b)=h(b))$	$\displaystyle\simeq\mathchoice{\prod_{b:B}\,}{\mathchoice{{\textstyle\prod_{(b% :B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle% \prod_{(b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{% \textstyle\prod_{(b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}\Bigl{(% }\mathopen{}\left\\|{\mathsf{fib}}_{f}(b)\right\\|\mathclose{}\to(g(b)=h(b))% \Bigr{)}$
		$\displaystyle\simeq\mathchoice{\prod_{b:B}\,}{\mathchoice{{\textstyle\prod_{(b% :B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle% \prod_{(b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{% \textstyle\prod_{(b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}\Bigl{(% }{\mathsf{fib}}_{f}(b)\to(g(b)=h(b))\Bigr{)}$
		$\displaystyle\simeq\mathchoice{\prod_{(b:B)}\,}{\mathchoice{{\textstyle\prod_{% (b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle% \prod_{(b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{% \textstyle\prod_{(b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}% \mathchoice{\prod_{(a:A)}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\mathchoice{\prod_{(p:f(a)% =b)}\,}{\mathchoice{{\textstyle\prod_{(p:f(a)=b)}}}{\prod_{(p:f(a)=b)}}{\prod_% {(p:f(a)=b)}}{\prod_{(p:f(a)=b)}}}{\mathchoice{{\textstyle\prod_{(p:f(a)=b)}}}% {\prod_{(p:f(a)=b)}}{\prod_{(p:f(a)=b)}}{\prod_{(p:f(a)=b)}}}{\mathchoice{{% \textstyle\prod_{(p:f(a)=b)}}}{\prod_{(p:f(a)=b)}}{\prod_{(p:f(a)=b)}}{\prod_{% (p:f(a)=b)}}}g(b)=h(b)$
		$\displaystyle\simeq\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle% \prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{% \textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\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 $\mathcal{S}et$ 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 orthogonal factorization system $(\mathcal{E},\mathcal{M})$ with $\mathcal{M}$ the monomorphisms, in which case $\mathcal{E}$ 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 $\mathcal{S}et$ are regular epis.

Proof.

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 $\mathcal{S}et$ being a regular category is that we have an “image” operation on subsets. That is, given $f:A\to B$ , any subset $P:\mathcal{P}(A)$ (i.e. a predicate $P:A\to\mathsf{Prop}$ ) has an image which is a subset of $B$ . This can be defined directly as $\setof{y:B|\exists(x:A).\,f(x)=y\land P(x)}$ , or indirectly as the image (in the previous sense) of the composite function

$\setof{x:A|P(x)}\to A\xrightarrow{f}B.$

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

Title	10.1.2 Images
\metatable