4.6 Surjections and embeddings
When $A$ and $B$ are sets and $f:A\to B$ is an equivalence, we also call it as isomorphism^{} 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\mathrm{:}A\mathrm{\to}B$.

1.
We say $f$ is surjective (or a surjection) if for every $b:B$ we have $\parallel {\mathrm{\U0001d5bf\U0001d5c2\U0001d5bb}}_{f}(b)\parallel $.

2.
We say $f$ is a embedding if for every $x,y:A$ the function ${\mathrm{\U0001d5ba\U0001d5c9}}_{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 ${\prod}_{(b:B)}{\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
$$\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 illbehaved notion for nonsets. 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\mathrm{:}A\mathrm{\to}B$ is an equivalence if and only if it is both surjective and an embedding.
Proof.
If $f$ is an equivalence, then each ${\mathrm{\U0001d5bf\U0001d5c2\U0001d5bb}}_{f}(b)$ is contractible^{}, hence so is $\parallel {\mathrm{\U0001d5bf\U0001d5c2\U0001d5bb}}_{f}(b)\parallel $, 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 ${\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 ${\mathrm{\U0001d5ba\U0001d5c9}}_{f}$ is an equivalence, there exists $r:x=y$ with ${\mathrm{\U0001d5ba\U0001d5c9}}_{f}(r)=p\text{centerdot}{q}^{1}$. However, using the characterization of paths in $\mathrm{\Sigma}$types, the latter equality rearranges to ${r}_{*}\left(p\right)=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\mathrm{:}A\mathrm{\to}B$ we have
$$\mathrm{\U0001d5c2\U0001d5cc\U0001d5be\U0001d5ca\U0001d5ce\U0001d5c2\U0001d5cf}(f)\simeq (\mathrm{\U0001d5c2\U0001d5cc\U0001d5a4\U0001d5c6\U0001d5bb\U0001d5be\U0001d5bd\U0001d5bd\U0001d5c2\U0001d5c7\U0001d5c0}(f)\times \mathrm{\U0001d5c2\U0001d5cc\U0001d5b2\U0001d5ce\U0001d5cb\U0001d5c3\U0001d5be\U0001d5bc\U0001d5cd\U0001d5c2\U0001d5cf\U0001d5be}(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 