# 10.1.2 Images

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

1. 1.

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

2. 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. 3.

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.

###### Lemma 10.1.1.

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

1. 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. 2.

(If $A$ has pullbacks) the diagonal map $a\to a\times_{b}a$

3. 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. 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)$

###### 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.

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. 1.

$f$ is an epimorphism.

2. 2.

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. 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. ∎

###### 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