# 4.6 Surjections and embeddings

When $A$ and $B$ are sets and $f:A\to B$ is an equivalence, we also call it as or a bijection. (We avoid these words for types that are not sets, since in homotopy theory and higher category theory they often denote a stricter notion of “sameness” than homotopy equivalence   .) In set theory  , a function is a bijection just when it is both injective  and surjective  . The same is true in type theory  , if we formulate these conditions appropriately. For clarity, when dealing with types that are not sets, we will speak of embeddings instead of injections.

###### Definition 4.6.1.

Let $f:A\to B$.

1. 1.

We say $f$ is surjective (or a surjection) if for every $b:B$ we have $\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right\|\mathclose{}$.

2. 2.

We say $f$ is a embedding if for every $x,y:A$ the function $\mathsf{ap}_{f}:(x=_{A}y)\to(f(x)=_{B}f(y))$ is an equivalence.

In other words, $f$ is surjective if every fiber of $f$ is merely inhabited, or equivalently if for all $b:B$ there merely exists an $a:A$ such that $f(a)=b$. In traditional logical notation, $f$ is surjective if $\forall(b:B).\,\exists(a:A).\,(f(a)=b)$. This must be distinguished from the stronger assertion that $\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{\sum_{(a:A)}\,% }{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A% )}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(% a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum% _{(a:A)}}}(f(a)=b)$; if this holds we say that $f$ is a split surjection.

If $A$ and $B$ are sets, then by Lemma 3.3.3 (http://planetmath.org/33merepropositions#Thmprelem2), $f$ is an embedding just when

 $\mathchoice{\prod_{x,y:A}\,}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(% x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle\prod_{(x,y% :A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{% \textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}% }(f(x)=_{B}f(y))\to(x=_{A}y).$ (4.6.2)

In this case we say that $f$ is injective, or an injection. We avoid these word for types that are not sets, because they might be interpreted as (4.6.2), which is an ill-behaved notion for non-sets. It is also true that any function between sets is surjective if and only if it is an epimorphism     in a suitable sense, but this also fails for more general types, and surjectivity is generally the more important notion.

###### Theorem 4.6.3.

A function $f:A\to B$ is an equivalence if and only if it is both surjective and an embedding.

###### Proof.

If $f$ is an equivalence, then each ${\mathsf{fib}}_{f}(b)$ is contractible  , hence so is $\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right\|\mathclose{}$, so $f$ is surjective. And we showed in Theorem 2.11.1 (http://planetmath.org/211identitytype#Thmprethm1) that any equivalence is an embedding.

Conversely, suppose $f$ is a surjective embedding. Let $b:B$; we show that $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}(f(x)=b)$ is contractible. Since $f$ is surjective, there merely exists an $a:A$ such that $f(a)=b$. Thus, the fiber of $f$ over $b$ is inhabited; it remains to show it is a mere proposition. For this, suppose given $x,y:A$ with $p:f(x)=b$ and $q:f(y)=b$. Then since $\mathsf{ap}_{f}$ is an equivalence, there exists $r:x=y$ with $\mathsf{ap}_{f}(r)=p\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}\mathord{{q}^{-1}}$. However, using the characterization of paths in $\Sigma$-types, the latter equality rearranges to ${r}_{*}\mathopen{}\left({p}\right)\mathclose{}=q$. Thus, together with $r$ it exhibits $(x,p)=(y,q)$ in the fiber of $f$ over $b$. ∎

###### Corollary 4.6.4.

For any $f:A\to B$ we have

 $\mathsf{isequiv}(f)\simeq(\mathsf{isEmbedding}(f)\times\mathsf{isSurjective}(f% )).$
###### Proof.

Being a surjection and an embedding are both mere propositions; now apply Lemma 3.3.3 (http://planetmath.org/33merepropositions#Thmprelem2). ∎

Of course, this cannot be used as a definition of “equivalence”, since the definition of embeddings refers to equivalences. However, this characterization can still be useful; see §8.8 (http://planetmath.org/88whiteheadstheoremandwhiteheadsprinciple). We will generalize it in http://planetmath.org/node/87580Chapter 7.

Title 4.6 Surjections and embeddings
\metatable