4.6 Surjections and embeddings

When A and B are sets and f:AB is an equivalence, we also call it as isomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath 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 equivalenceMathworldPlanetmathPlanetmath.) In set theoryMathworldPlanetmath, a function is a bijection just when it is both injectivePlanetmathPlanetmath and surjectivePlanetmathPlanetmath. The same is true in type theoryPlanetmathPlanetmath, 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:AB.

  1. 1.

    We say f is surjective (or a surjection) if for every b:B we have 𝖿𝗂𝖻f(b).

  2. 2.

    We say f is a embedding if for every x,y:A the function 𝖺𝗉f:(x=Ay)(f(x)=Bf(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 (b:B).(a:A).(f(a)=b). This must be distinguished from the stronger assertion that (b:B)(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

x,y:A(f(x)=Bf(y))(x=Ay). (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 epimorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmath 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:AB is an equivalence if and only if it is both surjective and an embedding.


If f is an equivalence, then each 𝖿𝗂𝖻f(b) is contractibleMathworldPlanetmath, hence so is 𝖿𝗂𝖻f(b), 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 (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 𝖺𝗉f is an equivalence, there exists r:x=y with 𝖺𝗉f(r)=p\centerdotq-1. However, using the characterization of paths in Σ-types, the latter equality rearranges to r*(p)=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:AB we have


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