I NTRODUCTION TO HOMOTOPY TYPE THEORY

E GBERT R IJKE

L ECTURE N OTES

FOR THE

S UMMER S CHOOL ON H OMOTOPY T YPE T HEORY

C ARNEGIE M ELLON U NIVERSITY

P ITTSBURGH PA

A UGUST 2019
 The author gratefully acknowledges the support of the Air Force Office of Scientific
Research through MURI grant FA9550-15-1-0053.

This work is licensed under a Creative Commons

“Attribution-NonCommercial-ShareAlike 4.0 International”
license.
Contents

Contents i

I Martin-Löf’s dependent type theory 1

1 Dependent type theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.1 Judgments and contexts in type theory . . . . . . . . . . . . . . . 1
1.2 Inference rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.3 Derivations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2 Dependent function types . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.1 Dependent function types . . . . . . . . . . . . . . . . . . . . . . . 8
2.2 Ordinary function types . . . . . . . . . . . . . . . . . . . . . . . . 10
2.3 The identity function, composition, and their laws . . . . . . . . . 10
Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
3 The natural numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
3.1 The formal specification of the type of natural numbers . . . . . . 14
3.2 Addition on the natural numbers . . . . . . . . . . . . . . . . . . . 16
Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
4 More inductive types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
4.1 The idea of general inductive types . . . . . . . . . . . . . . . . . 18
4.2 The unit type . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
4.3 The empty type . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
4.4 The booleans . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
4.5 Coproducts and the type of integers . . . . . . . . . . . . . . . . . 21
4.6 Dependent pair types . . . . . . . . . . . . . . . . . . . . . . . . . 23
4.7 Cartesian products . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
5 Identity types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
5.1 The inductive definition of identity types . . . . . . . . . . . . . . 27
5.2 The groupoidal structure of types . . . . . . . . . . . . . . . . . . 28
5.3 The action on paths of functions . . . . . . . . . . . . . . . . . . . 30
5.4 Transport . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
6 Type theoretic universes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
6.1 Specification of type theoretic universes . . . . . . . . . . . . . . . 34
6.2 Assuming enough universes . . . . . . . . . . . . . . . . . . . . . 35

i
ii CONTENTS

6.3 Pointed types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37

6.4 Families and relations on the natural numbers . . . . . . . . . . . 38
Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

II Basic concepts of type theory 41

7 Equivalences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
7.1 Homotopies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
7.2 Bi-invertible maps . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
7.3 The identity type of a Σ-type . . . . . . . . . . . . . . . . . . . . . 44
Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
8 Contractible types and contractible maps . . . . . . . . . . . . . . . . . . 49
8.1 Contractible types . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
8.2 Contractible maps . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
8.3 Equivalences are contractible maps . . . . . . . . . . . . . . . . . . 53
Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
9 The fundamental theorem of identity types . . . . . . . . . . . . . . . . . 57
9.1 Families of equivalences . . . . . . . . . . . . . . . . . . . . . . . . 57
9.2 The fundamental theorem . . . . . . . . . . . . . . . . . . . . . . . 60
9.3 Embeddings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
9.4 Disjointness of coproducts . . . . . . . . . . . . . . . . . . . . . . . 62
Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
10 The hierarchy of homotopical complexity . . . . . . . . . . . . . . . . . . 66
10.1 Propositions and subtypes . . . . . . . . . . . . . . . . . . . . . . . 66
10.2 Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
10.3 General truncation levels . . . . . . . . . . . . . . . . . . . . . . . 69
Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71

III Univalent mathematics 73

11 Function extensionality . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
11.1 Equivalent forms of function extensionality . . . . . . . . . . . . . 73
11.2 The type theoretic principle of choice . . . . . . . . . . . . . . . . 75
11.3 Universal properties . . . . . . . . . . . . . . . . . . . . . . . . . . 77
11.4 Composing with equivalences . . . . . . . . . . . . . . . . . . . . 78
Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
12 The univalence axiom . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
12.1 Equivalent forms of the univalence axiom . . . . . . . . . . . . . . 83
12.2 Univalence implies function extensionality . . . . . . . . . . . . . 84
12.3 Propositional extensionality and posets . . . . . . . . . . . . . . . 85
Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
13 Groups in univalent mathematics . . . . . . . . . . . . . . . . . . . . . . 88
13.1 Semi-groups and groups . . . . . . . . . . . . . . . . . . . . . . . . 88
13.2 Homomorphisms of semi-groups and groups . . . . . . . . . . . . 90
13.3 Isomorphic semi-groups are equal . . . . . . . . . . . . . . . . . . 91
13.4 Isomorphic groups are equal . . . . . . . . . . . . . . . . . . . . . 93
13.5 Categories in univalent mathematics . . . . . . . . . . . . . . . . . 93
Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
CONTENTS iii

14 The circle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
14.1 The induction principle of the circle . . . . . . . . . . . . . . . . . 96
14.2 The (dependent) universal property of the circle . . . . . . . . . . 97
14.3 Multiplication on the circle . . . . . . . . . . . . . . . . . . . . . . 100
Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
15 The fundamental cover of the circle . . . . . . . . . . . . . . . . . . . . . 104
15.1 Families over the circle . . . . . . . . . . . . . . . . . . . . . . . . . 104
15.2 The fundamental cover of the circle . . . . . . . . . . . . . . . . . 105
15.3 Contractibility of general total spaces . . . . . . . . . . . . . . . . 106
15.4 The dependent universal property of the integers . . . . . . . . . 108
15.5 The identity type of the circle . . . . . . . . . . . . . . . . . . . . . 110
Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111

Bibliography 113

Index 115
Chapter I

Martin-Löf’s dependent type theory

1 Dependent type theory

Dependent type theory is a system of inference rules that can be combined to make
derivations. In these derivations, the goal is often to construct a term of a certain type.
Such a term can be a function if the type of the constructed term is a function type; a
proof of a property if the type of the constructed term is a proposition; an identification if
the type of the constructed term is an identity type, and so on. In some respect, a type is
just a collection of mathematical objects and constructing terms of a type is the everyday
mathematical task or challenge. The system of inference rules that we call type theory
offers a principled way of engaging in mathematical activity.

1.1 Judgments and contexts in type theory

An inference rule is an expression of the form

H1 H2 ... Hn
C
containing above the horizontal line a finite list H1 , H2 , . . . , Hn of judgments for the
hypotheses, and below the horizontal line a single judgment C for the conclusion. A
very simple example that we will encounter in §2 when we introduce function types, is
the inference rule

Γ`a:A Γ` f :A→B
Γ ` f ( a) : B

This rule asserts that in any context Γ we may use a term a : A and a function f : A → B
to obtain a term f ( a) : B. Each of the expressions

Γ`a:A
Γ` f :A→B
Γ ` f ( a) : B

are examples of judgments. There are four kinds of judgments in type theory:

1
2 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

(i) A is a (well-formed) type in context Γ. The symbolic expression for this judgment is

Γ ` A type

(ii) A and B are judgmentally equal types in context Γ. The symbolic expression for this
judgment is
Γ ` A ≡ B type

(iii) a is a (well-formed) term of type A in context Γ. The symbolic expression for this
judgment is
Γ`a:A

(iv) a and b are judgmentally equal terms of type A in context Γ. The symbolic expression
for this judgment is
Γ`a≡b:A

Thus we see that any judgment is of the form Γ ` J , consisting of a context Γ and an
expression J asserting that A is a type, that A and B are equal types, that a is a term of
type A, or that a and b are equal terms of type A. The role of a context is to declare what
hypothetical terms are assumed, along with their types. More formally, a context is an
expression of the form

x 1 : A 1 , x 2 : A 2 ( x 1 ), . . . , x n : A n ( x 1 , . . . , x n −1 ) (1.1)

satisfying the condition that for each 1 ≤ k ≤ n we can derive, using the inference rules
of type theory, that

x1 : A1 , x2 : A2 ( x1 ), . . . , xk−1 : Ak−1 ( x1 , . . . , xk−2 ) ` Ak ( x1 , . . . , xk−1 ) type. (1.2)

In other words, to check that an expression of the form Eq. (1.1) is a context, one starts
on the left and works their way to the right verifying that each hypothetical term xk is
assigned a well-formed type. Hypothetical terms are commonly called variables, and we
say that a context as in Eq. (1.1) declares the variables x1 , . . . , xn . We may use variable
names other than x1 , . . . , xn , as long as no variable is declared more than once.
The condition in Eq. (1.2) that each of the hypothetical terms is assigned a well-formed
type, is checked recursively. Note that the context of length 0 satisfies the requirement in
Eq. (1.2) vacuously. This context is called the empty context. An expression of the form
x1 : A1 is a context if and only if A1 is a well-formed type in the empty context. Such
types are called closed types. We will soon encounter the type N of natural numbers,
which is an example of a closed type. There is also the notion of closed term, which
is simply a term in the empty context. The next case is that an expression of the form
x1 : A1 , x2 : A2 ( x1 ) is a context if and only if A1 is a well-formed type in the empty
context, and A2 ( x1 ) is a well-formed type, given a hypothetical term x1 : A1 . This
process repeats itself for longer contexts.
It is a feature of dependent type theory that all judgments are context-dependent, and
indeed that even the types of the variables may depend on any previously declared
variables. For example, when we introduce the identity type in §5, we make full use of
the machinery of type dependency, as is clear from how they are introduced:
1. DEPENDENT TYPE THEORY 3

Γ ` A type
Γ, x : A, y : A ` x = y type
This rule asserts that given a type A in context Γ, we may form a type x = y in context
Γ, x : A, y : A. Note that in order to know that the expression Γ, x : A, y : A is indeed a
well-formed context, we need to know that A is a well-formed type in context Γ, x : A.
This is an instance of weakening, which we will describe shortly.
In the situation where we have
Γ, x : A ` B( x ) type,
we say that B is a family of types over A in context Γ. Alternatively, we say that B( x ) is
a type indexed by x : A, in context Γ. Similarly, in the situation where we have
Γ, x : A ` b( x ) : B( x ),
we say that b is a section of the family B over A in context Γ. Alternatively, we say
that b( x ) is a term of type B( x ), indexed by x : A in context Γ. Note that in the above
situations A, B, and b also depend on the variables declared in the context Γ, even though
we have not explicitly mentioned them. It is common practice to not mention every
variable in the context Γ in such situations.

1.2 Inference rules

In this section we present the basic inference rules of dependent type theory. Those rules
are valid to be used in any type theoretic derivation. There are only four sets of inference
rules:
(i) Rules for judgmental equality
(ii) Rules for substitution
(iii) Rules for weakening
(iv) The “variable rule”

Judgmental equality
In this set of inference rules we ensure that judgmental equality (both on types and on
terms) are equivalence relations, and we make sure that in any context Γ, we can change
the type of any variable to a judgmentally equal type.
The rules postulating that judgmental equality on types and on terms is an equiva-
lence relation are as follows:
Γ ` A type Γ ` A ≡ A0 type Γ ` A ≡ A0 type Γ ` A0 ≡ A00 type
Γ ` A ≡ A type Γ ` A0 ≡ A type Γ ` A ≡ A00 type

Γ`a:A Γ ` a ≡ a0 : A Γ ` a ≡ a0 : A Γ ` a0 ≡ a00 : A
Γ`a≡a:A Γ ` a0 ≡ a : A Γ ` a ≡ a00 : A

Apart from the rules postulating that judgmental equality is an equivalence relation,
there are also variable conversion rules. Informally, these are rules stating that if A and
4 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

A0 are judgmentally equal types in context Γ, then any valid judgment in context Γ, x : A
is also a valid judgment in context Γ, x : A0 . In other words: we can convert the type of a
variable to a judgmentally equal type.
The first variable conversion rule states that

Γ ` A ≡ A0 type Γ, x : A, ∆ ` B( x ) type
Γ, x : A , ∆ ` B( x ) type
0

In this conversion rule, the context of the form Γ, x : A, ∆ is just any extension of the
context Γ, x : A.
Similarly, there are variable conversion rules for judgmental equality of types, for
terms, and for judgmental equality of terms. To avoid having to state essentially the
same rule four times, we state all four variable conversion rules at once using a generic
judgment J , which can be any of the four kinds of judgments.

Γ ` A ≡ A0 type Γ, x : A, ∆ ` J
Γ, x : A , ∆ ` J
0

An analogous term conversion rule, stated in Exercise 1.1, converting the type of a term to
a judgmentally equal type, is derivable using the rules for substitution and weakening,
and the variable rule.

Substitution
If we are given a term a : A in context Γ, then for any type B in context Γ, x : A, ∆ we can
form the type B[ a/x ] in context Γ, ∆[ a/x ], where B[ a/x ] is an abbreviation for

B ( x 1 , . . . , x n −1 , a ( x 1 , . . . , x n −1 ), x n +1 , . . . , x n + m −1 ).

This syntactic operation of substituting a for x is understood to be defined recursively

over the length of ∆. Similarly we obtain for any term b : B in context Γ, x : A, ∆ a
term b[ a/x ] : B[ a/x ]. The substitution rule asserts that substitution preserves well-
formedness and judgmental equality of types and terms:

Γ`a:A Γ, x : A, ∆ ` J
Sa
Γ, ∆[ a/x ] ` J [ a/x ]
Furthermore, we postulate that substitution by judgmentally equal terms results in
judgmentally equal types

Γ ` a ≡ a0 : A Γ, x : A, ∆ ` B type
Γ, ∆[ a/x ] ` B[ a/x ] ≡ B[ a0 /x ] type
and it also results in judgmentally equal terms

Γ ` a ≡ a0 : A Γ, x : A, ∆ ` b : B
Γ, ∆[ a/x ] ` b[ a/x ] ≡ b[ a0 /x ] : B[ a/x ]
When B is a family of types over A and a : A, we also say that B[ a/x ] is the fiber of B at
a. We will usually write B( a) for B[ a/x ].
1. DEPENDENT TYPE THEORY 5

Weakening
If we are given a type A in context Γ, then any judgment made in a longer context Γ, ∆
can also be made in the context Γ, x : A, ∆, for a fresh variable x. The weakening rule
asserts that weakening by a type A in context preserves well-formedness and judgmental
equality of types and terms.

Γ ` A type Γ, ∆ ` J
WA
Γ, x : A, ∆ ` J

This process of expanding the context by a fresh variable of type A is called weakening
(by A).
In the simplest situation where weakening applies, we have two types A and B in
context Γ. Then we can weaken B by A as follows

Γ ` A type Γ ` B type
WA
Γ, x : A ` B type

in order to form the type B in context Γ, x : A. The type B in context Γ, x : A is called the
constant family B, or the trivial family B.

The variable rule

If we are given a type A in context Γ, then we can weaken A by itself to obtain that A is
a type in context Γ, x : A. The variable rule now asserts that any hypothetical term x : A
in context Γ is a well-formed term of type A in context Γ, x : A.

Γ ` A type
δ
Γ, x : A ` x : A A

One of the reasons for including the variable rule is that it provides an identity function
on the type A in context Γ.

1.3 Derivations
A derivation in type theory is a tree in which each node is a valid rule of inference. We
give two examples of derivations: a derivation showing that any variable can be changed
to a fresh one, and a derivation showing that any two variables that do not depend on
one another can be swapped in order.
Thus, we will see some examples of new inference rules that can be derived using
the rules of type theory. Such inference rules are called admissible. Since derivations
tend to get long and unwieldy, we declare that admissible inference rules are also valid
to be used in derivations.
6 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

Changing variables
Variables can always be changed to fresh variables. We show that this is the case by
showing that the inference rule

Γ, x : A, ∆ ` J
x 0 /x
Γ, x 0 : A, ∆[ x 0 /x ] ` J [ x 0 /x ]

is admissible, where x 0 is a variable that does not occur in the context Γ, x : A, ∆.

Indeed, we have the following derivation using substitution, weakening, and the
variable rule:

Γ ` A type Γ ` A type Γ, x : A, ∆ ` J
δA WA
Γ, x : A ` x : A
0 0 Γ, x : A, x : A, ∆ ` J
0
Sx 0
Γ, x 0 : A, ∆[ x 0 /x ] ` J [ x 0 /x ]

In this derivation it is the application of the weakening rule where we have to check that
x 0 does not occur in the context Γ, x : A, ∆.

Interchanging variables
The interchange rule states that if we have two types A and B in context Γ, and we
make a judgment in context Γ, x : A, y : B, ∆, then we can make that same judgment in
context Γ, y : B, x : A, ∆ where the order of x : A and y : B is swapped. More formally,
the interchange rule is the following inference rule

Γ ` B type Γ, x : A, y : B, ∆ ` J
Γ, y : B, x : A, ∆ ` J

Just as the rule for changing variables, we claim that the interchange rule is an admissible
rule.
The idea of the derivation for the interchange rule is as follows: If we have a judgment

Γ, x : A, y : B, ∆ ` J ,

then we can change the variable y to a fresh variable y0 and weaken the judgment to
obtain the judgment

Γ, y : B, x : A, y0 : B, ∆[y0 /y] ` J [y0 /y].

Now we can substitute y for y0 to obtain the desired judgment Γ, y : B, x : A, ∆ ` J . The

formal derivation is as follows:

Γ ` B type Γ, x : A, y : B, ∆ ` J
δB y0 /y
Γ, y : B ` y : B Γ, x : A, y0 : B, ∆[y0 /y] ` J [y0 /y]
WWB ( A) WB
Γ, y : B, x : A ` y : B Γ, y : B, x : A, y0 : B, ∆[y0 /y] ` J [y0 /y]
SWA (y)
Γ, y : B, x : A, ∆ ` J
1. EXERCISES 7

Exercises
1.1 Give a derivation for the following term conversion rule:

Γ ` A ≡ A0 type Γ`a:A
Γ`a:A 0

1.2 Consider a type A in context Γ. In this exercise we establish a correspondence

between types in context Γ, x : A, and uniform choices of types Ba , where a ranges
over terms of A in a uniform way. A similar connection is made for terms.
(a) We define a uniform family over A to consist of a type

∆, Γ ` Ba type

for every context ∆, and every term ∆, Γ ` a : A, subject to the condition that
one can derive

∆`d:D ∆, y : D, Γ ` a : A
∆, Γ ` Ba [d/y] ≡ Ba[d/y] type
Define a bijection between the set of types in context Γ, x : A modulo judg-
mental equality, and the set of uniform families over A modulo judgmental
equality.
(b) Consider a type Γ, x : A ` B. We define a uniform term of B over A to consist
of a type
∆, Γ ` ba : B[ a/x ] type

for every context ∆, and every term ∆, Γ ` a : A, subject to the condition that
one can derive

∆`d:D ∆, y : D, Γ ` a : A
∆, Γ ` ba [d/y] ≡ ba[d/y] : B[ a/x ][d/y]
Define a bijection between the set of terms of B in context Γ, x : A mod-
ulo judgmental equality, and the set of uniform terms of B over A modulo
judgmental equality.

2 Dependent function types

A fundamental concept in dependent type theory is that of a dependent function. A
dependent function is a function of which the type of the output may depend on the
input. They are a generalization of ordinary functions, because an ordinary function
f : A → B is a function of which the output f ( x ) has type B regardless of the value of x.
8 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

2.1 Dependent function types

Consider a section b of a family B over A in context Γ, i.e.,
Γ, x : A ` b( x ) : B( x ).
From one point of view, such a section b is an operation, or a program, that takes as input
x : A and produces a term b( x ) : B( x ). From a more mathematical point of view we see
b as a choice of an element of each B( x ). In other words, we may see b as a function that
takes x : A to b( x ) : B( x ). Note that the type B( x ) of the output is dependent on x : A.
In this section we postulate rules for the type of all such dependent functions: whenever
B is a family over A in context Γ, there is a type

∏ (x:A) B( x )
in context Γ, consisting of all the dependent functions of which the output at x : A has
type B( x ). There are four principal rules for Π-types:
(i) The formation rule, which tells us how we may form dependent function types.
(ii) The introduction rule, which tells us how to introduce new terms of dependent
function types.
(iii) The elimination rule, which tells us how to use arbitrary terms of dependent
function types.
(iv) The computation rules, which tell us how the introduction and elimination rules
interact. These computation rules guarantee that every term of a dependent
function type behaves as expected: as a dependent function.
In the cases of the formation rule, the introduction rule, and the elimination rule, we will
also provide conversion rules that ensure that all the constructions respect judgmental
equality.

The Π-formation rule

Dependent function types are formed by the following Π-formation rule:

Γ, x : A ` B( x ) type
Π.
Γ ` ∏ (x:A) B( x ) type
With the following conversion rule we postulate that formation of dependent function
types respects judgmental equality of types:

Γ ` A ≡ A0 type Γ, x : A ` B( x ) ≡ B0 ( x ) type
Π-eq.
Γ ` ∏ (x:A) B( x ) ≡ ∏ (x:A0 ) B0 ( x ) type

Furthermore, when x 0 is a fresh variable, i.e., which does not occur in the context Γ, x : A,
we also postulate that

Γ, x : A ` B( x ) type
Π-x 0 /x.
Γ ` ∏ (x:A) B( x ) ≡ ∏ (x0 :A) B( x 0 ) type
2. DEPENDENT FUNCTION TYPES 9

The Π-introduction rule

The introduction rule for dependent function types is also called the λ-abstraction rule.
Recall that dependent functions are formed from terms b( x ) of type B( x ) in context
Γ, x : A. Therefore the λ-abstraction rule is as follows:

Γ, x : A ` b( x ) : B( x )
λ
Γ ` λx. b( x ) : ∏ (x:A) B( x )

Just like ordinary mathematicians, we will sometimes write x 7→ f ( x ) for a function f .

The map n 7→ n2 is an example. The λ-abstraction is also required to respect judgmental
equality. Therefore we postulate the λ-conversion rule, which asserts that

Γ, x : A ` b( x ) ≡ b0 ( x ) : B( x )
λ-eq.
Γ ` λx. b( x ) ≡ λx. b0 ( x ) : ∏ (x:A) B( x )

The Π-elimination rule

The elimination rule for dependent function types provides us with a way to use depen-
dent functions. The way to use a dependent function is to apply it to an argument of
the domain type. The Π-elimination rule is therefore also called the evaluation rule. It
asserts that given a dependent function f : ∏ (x:A) B( x ) in context Γ we obtain a term
f ( x ) of type B( x ) in context Γ, x : A. More formally:

Γ ` f : ∏ (x:A) B( x )
ev
Γ, x : A ` f ( x ) : B( x )

Again we require that evaluation respects judgmental equality:

Γ ` f ≡ f 0 : ∏ (x:A) B( x )
Γ, x : A ` f ( x ) ≡ f 0 ( x ) : B( x )

The Π-computation rules

The computation rules for dependent function types postulate that λ-abstraction rule
and the evaluation rule are mutual inverses. Thus we have two computation rules.
First we postulate the β-rule

Γ, x : A ` b( x ) : B( x )
β.
Γ, x : A ` (λy.b(y))( x ) ≡ b( x ) : B( x )

Second, we postulate the η-rule

Γ ` f : ∏ (x:A) B( x )
η.
Γ ` λx. f ( x ) ≡ f : ∏ (x:A) B( x )

This completes the specification of dependent function types.

10 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

2.2 Ordinary function types

In the case where both A and B are types in context Γ, we may first weaken B by A, and
then apply the formation rule for the dependent function type:

Γ ` A type Γ ` B type
Γ, x : A ` B type
Γ ` ∏ (x:A) B type

The result is the type of functions that take an argument of type A, and return a term of
type B. In other words, terms of the type ∏ (x:A) B are ordinary functions from A to B. We
write A → B for the type of functions from A to B. Sometimes we will also write B A for
the type A → B.
We give a brief summary of the rules specifying ordinary function types, omitting
the conversion rules. All of these rules can be derived easily from the corresponding
rules for Π-types.

Γ ` A type Γ ` B type
→
Γ ` A → B type

Γ ` B type Γ, x : A ` b( x ) : B Γ` f :A→B
λ ev
Γ ` λx. b( x ) : A → B Γ, x : A ` f ( x ) : B

Γ ` B type Γ, x : A ` b( x ) : B Γ` f :A→B
β η
Γ, x : A ` (λy. b(y))( x ) ≡ b( x ) : B Γ ` λx. f ( x ) ≡ f : A → B

2.3 The identity function, composition, and their laws

Definition 2.3.1. For any type A in context Γ, we define the identity function id A : A →
A using the variable rule:

Γ ` A type
Γ, x : A ` x : A
Γ ` id A :≡ λx. x : A → A
Note that we have used the symbol ≡ in the conclusion to define the identity function.
A judgment of the form Γ ` a :≡ b : A should be read as "b is a well-defined term of type
A in context Γ, and we will refer to it as a".

Definition 2.3.2. For any three types A, B, and C in context Γ, there is a composition
operation
comp : ( B → C ) → (( A → B) → ( A → C )),
i.e., we can derive

Γ ` A type Γ ` B type Γ ` C type

Γ ` comp : ( B → C ) → (( A → B) → ( A → C ))
We will write g ◦ f for comp( g, f ).
2. DEPENDENT FUNCTION TYPES 11

Construction. The idea of the definition is to define comp( g, f ) to be the function λx. g( f ( x )).
The derivation we use to construct comp is as follows:
Γ ` B type Γ ` C type
Γ ` A type Γ ` B type Γ, g : CB, y : B ` g(y) : C
Γ, f : BA, x : A ` f (x) : B Γ, g : CB, f : BA, y : B ` g(y) : C
Γ, g : CB, f : BA, x : A ` f (x) : B Γ, g : CB, f : BA, x : A, y : B ` g(y) : C
Γ, g : C B , f : B A , x : A ` g( f ( x )) : C
Γ, g : C B , f : B A ` λx. g( f ( x )) : C A
Γ, g : B → C ` λ f . λx. g( f ( x )) : B A → C A
Γ ` comp :≡ λg. λ f . λx. g( f ( x )) : C B → ( B A → C A )

The rules of function types can be used to derive the laws of a category for functions,
i.e., we can derive that function composition is associative and that the identity function
satisfies the unit laws. In the remainder of this section we will give these derivations.

Lemma 2.3.3. Composition of functions is associative, i.e., we can derive

Γ` f :A→B Γ`g:B→C Γ`h:C→D

Γ ` (h ◦ g) ◦ f ≡ h ◦ ( g ◦ f ) : A → D
Proof. The main idea of the proof is that both ((h ◦ g) ◦ f )( x ) and (h ◦ ( g ◦ f ))( x ) evaluate
to h( g( f ( x )), and therefore (h ◦ g) ◦ f and h ◦ ( g ◦ f ) must be judgmentally equal. This
idea is made formal in the following derivation:

Γ`g:B→C
Γ` f :A→B Γ, y : B ` g(y) : C Γ`h:C→D
Γ, x : A ` f ( x ) : B Γ, x : A, y : B ` g(y) : C Γ, z : C ` h(z) : D
Γ, x : A ` g( f ( x )) : C Γ, x : A, z : C ` h(z) : D
Γ, x : A ` h( g( f ( x ))) : D
Γ, x : A ` h( g( f ( x ))) ≡ h( g( f ( x ))) : D
Γ, x : A ` (h ◦ g)( f ( x )) ≡ h(( g ◦ f )( x )) : D
Γ, x : A ` ((h ◦ g) ◦ f )( x ) ≡ (h ◦ ( g ◦ f ))( x ) : D
Γ ` (h ◦ g) ◦ f ≡ h ◦ ( g ◦ f ) : A → D.

Lemma 2.3.4. Composition of functions satisfies the left and right unit laws, i.e., we can derive

Γ` f :A→B
Γ ` idB ◦ f ≡ f : A → B
and
Γ` f :A→B
Γ ` f ◦ id A ≡ f : A → B
12 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

Proof. The derivation for the left unit law is

Γ ` B type
Γ` f :A→B Γ, y : B ` idB (y) ≡ y : B
Γ, x : A ` f ( x ) : B Γ, x : A, y : B ` idB (y) ≡ y : B
Γ, x : A ` idB ( f ( x )) ≡ f ( x ) : B
Γ, x : A ` (idB ◦ f )( x ) ≡ f ( x ) : B
Γ ` idB ◦ f ≡ f : A → B
The right unit law is left as Exercise 2.1.

Exercises
2.1 Give a derivation for the right unit law of Lemma 2.3.4.
2.2 Show that the rule

Γ, x : A ` b( x ) : B( x )
λ-x 0 /x
Γ ` λx. b( x ) ≡ λx 0 . b( x 0 ) : ∏ (x:A) B( x )

is admissible for any variable x 0 that does not occur in the context Γ, x : A.
2.3 (a) Construct the constant function
Γ ` A type
Γ, y : B ` consty : A → B
(b) Show that
Γ` f :A→B
Γ, z : C ` constz ◦ f ≡ constz : A → C
(c) Show that
Γ ` A type Γ`g:B→C
Γ, y : B ` g ◦ consty ≡ constg(y) : A → C
2.4 In this exercise we generalize the composition operation of non-dependent function
types:
(a) Define a composition operation for dependent function types
Γ ` f : ∏ (x:A) B( x ) Γ ` g : ∏ (x:A) ∏ (y:B(x)) C ( x, y)
Γ` g ◦0 f : ∏ (x:A) C ( x, f ( x ))
and show that this operation agrees with ordinary composition when it is
specialized to non-dependent function types.
(b) Show that composition of dependent functions agrees with ordinary compo-
sition of functions:
Γ` f :A→B Γ`g:B→C
Γ ` (λx. g) ◦ f ≡ g ◦ f : A → C
0

(c) Show that composition of dependent functions is associative.

(d) Show that composition of dependent functions satisfies the right unit law:
3. THE NATURAL NUMBERS 13

Γ ` f : ∏ (x:A) B( x )
Γ ` (λx. f ) ◦0 id A ≡ f : ∏ (x:A) B( x )
(e) Show that composition of dependent functions satisfies the left unit law:
Γ ` f : ∏ (x:A) B( x )
Γ ` (λx. idB(x) ) ◦0 f ≡ f : ∏ (x:A) B( x )
2.5 (a) Given two types A and B in context Γ, and a type C in context Γ, x : A, y : B,
define the swap function
   
Γ ` σ : ∏ (x:A) ∏ (y:B) C ( x, y) → ∏ (y:B) ∏ (x:A) C ( x, y)

that swaps the order of the arguments.

(b) Show that
   
Γ ` σ ◦ σ ≡ id : ∏ (x:A) ∏ (y:B) C ( x, y) → ∏ (x:A) ∏ (y:B) C ( x, y) .

3 The natural numbers

The set of natural numbers is the most important object in mathematics. We quote Bishop,
from his Constructivist Manifesto, the first chapter in Foundations of Constructive
Analysis [1], where he gives a colorful illustration of its importance to mathematics.

“The primary concern of mathematics is number, and this means the positive
integers. We feel about number the way Kant felt about space. The positive
integers and their arithmetic are presupposed by the very nature of our
intelligence and, we are tempted to believe, by the very nature of intelligence
in general. The development of the theory of the positive integers from
the primitive concept of the unit, the concept of adjoining a unit, and the
process of mathematical induction carries complete conviction. In the words
of Kronecker, the positive integers were created by God. Kronecker would
have expressed it even better if he had said that the positive integers were
created by God for the benefit of man (and other finite beings). Mathematics
belongs to man, not to God. We are not interested in properties of the
positive integers that have no descriptive meaning for finite man. When a
man proves a positive integer to exist, he should show how to find it. If God
has mathematics of his own that needs to be done, let him do it himself.”

A bit later in the same chapter, he continues:

“Building on the positive integers, weaving a web of ever more sets and
ever more functions, we get the basic structures of mathematics: the ra-
tional number system, the real number system, the euclidean spaces, the
complex number system, the algebraic number fields, Hilbert space, the
classical groups, and so forth. Within the framework of these structures, most
mathematics is done. Everything attaches itself to number, and every math-
ematical statement ultimately expresses the fact that if we perform certain
computations within the set of positive integers, we shall get certain results.”
14 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

3.1 The formal specification of the type of natural numbers

The type N of natural numbers is the archetypal example of an inductive type. The
rules we postulate for the type of natural numbers come in four sets, just as the rules for
Π-types:
(i) The formation rule, which asserts that the type N can be formed.
(ii) The introduction rules, which provide the zero element and the successor function.
(iii) The elimination rule. This rule is the type theoretic analogue of the induction
principle for N.
(iv) The computation rules, which assert that any application of the elimination rule
behaves as expected on the constructors 0N and succN of N.

The formation rule of N

The type N is formed by the N-formation rule
N-form
` N type.
In other words, N is postulated to be a closed type.

The introduction rules of N

Unlike the set of positive integers in Bishop’s remarks, Peano’s first axiom postulates
that 0 is a natural number. The introduction rules for N equip it with the zero term and
the successor function.

` 0N : N ` succN : N → N

Remark 3.1.1. We annotate the terms 0N and succN of type N with their type in the
subscript, as a reminder that 0N and succN are declared to be terms of type N, and not
of any other type. In the next chapter we will introduce the type Z of the integers, on
which we can also define a zero term 0Z , and a successor function succZ . These should
be distinguished from the terms 0N and succN . In general, we will make sure that every
term is given a unique name. In libraries of mathematics formalized in a computer proof
assistant it is also the case that every type must be given a unique name.

The elimination rule of N

To prove properties about the natural numbers, we postulate an induction principle for N.
For a typical example, it is easy to show by induction that
n ( n + 1)
1+···+n = .
2
Similarly, we can define operations by recursion on the natural numbers: the Fibonacci
sequence is defined by F (0) = 0, F (1) = 1, and
F ( n + 2) = F ( n ) + F ( n + 1).
3. THE NATURAL NUMBERS 15

Needless to say, we want an induction principle to hold for the natural numbers in type
theory and we also want it to be possible to construct operations on the natural numbers
by recursion.
In dependent type theory we may think of a type family P over N as a predicate over
N. Especially after we introduce a few more type-forming operations, such as Σ-types
and identity types, it will become clear that the language of dependent type theory
expressive enough to find definitions of all of the standard concepts and operations
of elementary number theory in type theory. Many of those definitions, the ordering
relations ≤ and < for example, will make use of type dependency. Then, to prove that
P(n) ‘holds’ for all n we just have to construct a dependent function

∏ (n:N) P(n).
The induction principle for the natural numbers in type theory exactly states what
one has to do in order to construct such a dependent function, via the following inference
rule:
Γ, n : N ` P(n) type
Γ ` p 0 : P ( 0N )
Γ ` pS : ∏ (n:N) P(n) → P(succN (n))
N-ind
Γ ` indN ( p0 , pS ) : ∏ (n:N) P(n)
Just like for the usual induction principle of the natural numbers, there are two things
to be constructed given a type family P over N: in the base case we need to construct
a term p0 : P(0N ), and for the inductive step we need to construct a function of type
P(n) → P(succN (n)) for all n : N. And this comes at one immediate advantage:
induction and recursion in type theory are one and the same thing!
Remark 3.1.2. We might alternatively present the induction principle of N as the following
inference rule
Γ, n : N ` P(n) type
  
Γ ` indN : P(0N ) → ∏ (n:N) P(n) → P(succN (n)) → ∏ (n:N) P(n)

In other words, for any type family P over N there is a function indN that takes two
arguments, one for the base case and one for the inductive step, and returns a section
of P. Now it is justified to wonder: is this slightly different presentation of induction
equivalent to the previous presentation?
To see that indeed we get such a function from the induction principle (rule N-ind
above), we note that the induction principle is stated to hold in an arbitrary context Γ. So
let us wield the power of type dependency: by weakening and the variable rule we have
the following well-formed terms:

Γ, p0 : P(0N ), pS : ∏ (n:N) P(n) → P(succN (n)) ` p0 : P(0N )

Γ, p0 : P(0N ), pS : ∏ (n:N) P(n) → P(succN (n)) ` pS : ∏ (n:N) P(n) → P(succN (n)).

Therefore, the induction principle of N provides us with a term

Γ, p0 : P(0N ), pS : ∏ (n:N) P(n) → P(succN (n)) ` indN ( p0 , pS ) : ∏ (n:N) P(n).

16 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

By λ-abstraction we now obtain a function

  
indN : P(0N ) → ∏ (n:N) P(n) → P(succN (n)) → ∏ (n:N) P(n)

in context Γ. Therefore we see that it does not really matter whether we present the
induction principle of N in a more verbose way as an inference rule with the base case
and the inductive step as hypotheses, or as a function taking variables for the base case
and the inductive step as arguments.

The computation rules of N

The computation rules for N postulate that the dependent function indN ( P, p0 , pS )
behaves as expected when it is applied to 0N or a successor. There is one computation
rule for each step in the induction principle, covering the base case and the inductive
step.
The computation rule for the base case is

Γ, n : N ` P(n) type
Γ ` p 0 : P ( 0N )
Γ ` pS : ∏ (n:N) P(n) → P(succN (n))
Γ ` indN ( p0 , pS , 0N ) ≡ p0 : P(0N )
Similarly, with the same hypotheses as for the computation rule for the base case, the
computation rule for the inductive step is

···
Γ, n : N ` indN ( p0 , pS , succN (n)) ≡ pS (n, indN ( p0 , pS , n)) : P(succN (n))
This completes the formal specification of N.

3.2 Addition on the natural numbers

Using the induction principle of N we can perform many familiar constructions. For
instance, we can define the addition operation by induction on N.

Definition 3.2.1. We define a function

addN : N → (N → N)

satisfying addN (0N , n) ≡ n and addN (succN (m), n) ≡ succN (addN (m, n)). Usually we
will write n + m for addN (n, m).

Informal construction. Informally, the definition of addition is as follows. By induction it

suffices to construct a function add-0N : N → N, and a function

add-succN (n, f ) : N → N,

for every n : N and every f : N → N.

3. THE NATURAL NUMBERS 17

The function add-0N : N → N is of course taken to be idN , since the result of adding
0 to n should be n.
Given n : N and a function f : N → N we define add-succN (n, f ) :≡ succN ◦ f . The
idea is that if f represents adding m, then add-succN (n, f ) should be adding one more
than f did.
Formal derivation. The derivation for the construction of add-succN looks as follows:

` N type ` N type ` N type

` comp : N → (N → NN )
N N

succN : NN g : N → N ` comp( g) : NN → NN
` comp(succN ) : NN → NN
n : N ` comp(succN ) : NN → NN
` add-succN :≡ λn. comp(succN ) : N → (NN → NN )
We combine this derivation with the induction principle of N to complete the construc-
tion of addition:
.. .. ..
. . .
n : N ` NN type ` add-0N :≡ idN : NN ` add-succN : N → (NN → NN )
` addN ≡ indN (add-0N , add-succN ) : N → NN
The asserted judgmental equalities then hold by the computation rules for N.
Remark 3.2.2. When we define a function f : ∏ (n:N) P(n), we will often do so just by
indicating its definition on 0N and its definition on succN (n), by writing
f (0N ) :≡ p0
f (succN (n)) :≡ pS (n, f (n)).
For example, the definition of addition on the natural numbers could be given as
addN (0N , n) :≡ n
addN (succN (m), n) :≡ succN (addN (m, n)).
This way of defining a function is called pattern matching. A more formal inductive
argument can be obtained from a definition by pattern matching if it is possible to obtain
from the expression pS (n, f (n)) a general dependent function
pS : ∏ (n:N) P(n) → P(succN (n)).
In practice this is usually the case. Computer proof assistants such as Agda have
sophisticated algorithms to allow for definitions by pattern matching.
Remark 3.2.3. By the computation rules for N it follows that
0N + n ≡ n, and succN (m) + n ≡ succN (m + n).
However, the rules that we provided so far are not sufficient to also conclude that n +
0N ≡ n and n + succN (m) ≡ succN (n + m). Nevertheless, once we have introduced the
identity type in §5 we will nevertheless be able to identify n + 0N with n, and n + succN (m)
with succN (n + m). See Exercise 5.5.
18 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

Exercises
3.1 Define the binary min and max functions

minN , maxN : N → (N → N).

3.2 Define the multiplication operation

mulN : N → (N → N).

3.3 Define the exponentiation function n, m 7→ mn of type N → (N → N).

3.4 Define the factorial operation n 7→ n!.
3.5 Define the binomial coefficient (nk) for any n, k : N, making sure that (nk) ≡ 0 when
n < k.
3.6 Define the Fibonacci sequence 0, 1, 1, 2, 3, 5, 8, 13, . . . as a function F : N → N.

4 More inductive types

Analogous to the type of natural numbers, many types can be specified as inductive
types. In this lecture we introduce some further examples of inductive types: the unit
type, the empty type, the booleans, coproducts, dependent pair types, and cartesian
products. We also introduce the type of integers.

4.1 The idea of general inductive types

Just like the type of natural numbers, other inductive types are also specified by their
constructors, an induction principle, and their computation rules:

(i) The constructors tell what structure the inductive type comes equipped with.
There may any finite number of constructors, even no constructors at all, in the
specification of an inductive type.

(ii) The induction principle specifies the data that should be provided in order to
construct a section of an arbitrary type family over the inductive type.

(iii) The computation rules assert that the inductively defined section agrees on the
constructors with the data that was used to define the section. Thus, there is a
computation rule for every constructor.

The induction principle and computation rules can be generated automatically once the
constructors are specified, but it goes beyond the scope of our course to describe general
inductive types.

4.2 The unit type

A straightforward example of an inductive type is the unit type, which has just one
constructor. Its induction principle is analogous to just the base case of induction on the
natural numbers.
4. MORE INDUCTIVE TYPES 19

Definition 4.2.1. We define the unit type to be a closed type 1 equipped with a closed
term
? : 1,
satisfying the induction principle that for any type family of types P( x ) indexed by x : 1,
there is a term
ind1 : P(?) → ∏ (x:1) P( x )
for which the computation rule
ind1 ( p, ?) ≡ p
holds. Sometimes we write λ ? . p for ind1 ( p).

The induction principle can also be used to define ordinary functions out of the unit
type. Indeed, given a type A we can first weaken it to obtain the constant family over 1,
with value A. Then the induction principle of the unit type provides a function

ind1 : A → (1 → A).

In other words, by the induction principle for the unit type we obtain for every x : A a
function ptx :≡ ind1 ( x ) : 1 → A.

4.3 The empty type

The empty type is a degenerate example of an inductive type. It does not come equipped
with any constructors, and therefore there are also no computation rules. The induction
principle merely asserts that any type family has a section. In other words: if we assume
the empty type has a term, then we can prove anything.

Definition 4.3.1. We define the empty type to be a type ∅ satisfying the induction
principle that for any family of types P( x ) indexed by x :, there is a term

ind∅ : ∏ (x:∅) P( x ).

The induction principle for the empty type can also be used to construct a function

∅→A

for any type A. Indeed, to obtain this function one first weakens A to obtain the constant
family over ∅ with value A, and then the induction principle gives the desired function.
Thus we see that from the empty type anything follows. Therefore, we we see that
anything follows from A, if we have a function from A to the empty type. This motivates
the following definition.

Definition 4.3.2. For any type A we define negation of A by

¬ A :≡ A → ∅.

Since ¬ A is the type of functions from A to ∅, a proof of ¬ A is given by assuming

that A holds, and then deriving a contradiction. This proof technique is called proof of
negation. Proofs of negation are not to be confused with proofs by contradiction. In type
theory there is no way of obtaining a term of type A from a term of type ( A → ∅) → ∅.
20 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

4.4 The booleans

Definition 4.4.1. We define the booleans to be a type 2 that comes equipped with

02 : 2
12 : 2

satisfying the induction principle that for any family of types P( x ) indexed by x : 2,
there is a term  
ind2 : P(02 ) → P(12 ) → ∏ (x:2) P( x )

for which the computation rules

ind2 ( p0 , p1 , 02 ) ≡ p0
ind2 ( p0 , p1 , 12 ) ≡ p1

hold.

Just as in the cases for the unit type and the empty type, the induction principle for
the booleans can also be used to construct an ordinary function 2 → A, provided that we
can construct two terms of type A. Indeed, by the induction principle for the booleans
there is a function
ind2 : A → ( A → A2 )
for any type A.
Example 4.4.2. Using the induction principle of 2 we can define all the operations of
Boolean algebra. For example, the boolean negation operation neg2 : 2 → 2 is defined
by

neg2 (12 ) :≡ 02 neg2 (02 ) :≡ 12 .

The boolean conjunction operation – ∧ – : 2 → (2 → 2) is defined by

12 ∧ 12 : ≡ 12 02 ∧ 12 : ≡ 02
12 ∧ 02 : ≡ 02 02 ∧ 02 : ≡ 02 .

The boolean disjunction operation – ∨ – : 2 → (2 → 2) is defined by

12 ∨ 12 : ≡ 12 02 ∨ 12 : ≡ 12
12 ∨ 02 : ≡ 12 02 ∨ 02 : ≡ 02 .

We leave the definitions of some of the other boolean operations as Exercise 4.3. Note
that the method of defining the boolean operations by the induction principle of 2 is not
that different from defining them by truth tables.
Boolean logic is important, but it won’t be very prominent in this course. The reason
is simple: in type theory it is more natural to use the ‘logic’ of types that is provided by
the inference rules.
4. MORE INDUCTIVE TYPES 21

4.5 Coproducts and the type of integers

Definition 4.5.1. Let A and B be types. We define the coproduct A + B to be a type that
comes equipped with

inl : A → A + B
inr : B → A + B

satisfying the induction principle that for any family of types P( x ) indexed by x : A + B,
there is a term
   
ind+ : ∏ (x:A) P(inl( x )) → ∏ (y:B) P(inr(y)) → ∏ (z:A+ B) P(z)

for which the computation rules

ind+ ( f , g, inl( x )) ≡ f ( x )
inr+( f , g, inr(y)) ≡ g(y)

hold. Sometimes we write [ f , g] for ind+ ( f , g).

The coproduct of two types is sometimes also called the disjoint sum. By the
induction principle of coproducts it follows that we have a function


( A → X) → (B → X) → ( A + B → X)
for any type X. Note that this special case of the induction principle of coproducts is
very much like the elimination rule of disjunction in first order logic: if P, P0 , and Q are
propositions, then we have

( P → Q) → ( P0 → Q) → ( P ∨ P0 → Q) .

Indeed, we can think of propositions as types and of terms as their constructive proofs.
Under this interpretation of type theory the coproduct is indeed the disjunction.
An important example of a type that can be defined using coproducts is the type Z
of integers.
Definition 4.5.2. We define the integers to be the type Z :≡ N + (1 + N). The type of
integers comes equipped with inclusion functions of the positive and negative integers

in-pos :≡ inr ◦ inr

in-neg :≡ inl,

which are both of type N → Z, and the constants

−1Z :≡ in-neg(0)
0Z :≡ inr(inl(?))
1Z :≡ in-pos(0).

In the following lemma we derive an induction principle for Z, which can be used in
many familiar constructions on Z, such as in the definitions of addition and multiplica-
tion.
22 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

Lemma 4.5.3. Consider a type family P over Z. If we are given

p−1 : P(−1Z )
p−S : ∏ (n:N) P(in-neg(n)) → P(in-neg(succN (n)))
p 0 : P ( 0Z )
P1 : P(1Z )
PS : ∏ (n:N) P(in-pos(n)) → P(in-pos(succN (n))),

then we can construct a dependent function f : ∏ (k:Z) P(k ) for which the following judgmental
equalities hold:

f (−1Z ) ≡ p−1
f (in-neg(succN (n))) ≡ p−S (n, f (in-neg(n)))
f ( 0Z ) ≡ p 0
f (1Z ) ≡ p1
f (in-pos(succN (n))) ≡ pS (n, f (in-pos(n))).

Proof. Since Z is the coproduct of N and 1 + N, it suffices to define

pinl : ∏ (n:N) P(inl(n))

pinr : ∏ (t:1+N) P(inr(t)).

Note that in-neg ≡ inl and −1Z ≡ in-neg(0N ). In order to define pinl we use induction
on the natural numbers, so it suffices to define

p−1 : P(−1)
p−S : ∏ (n:N) P(in-neg(n)) → P(in-neg(succN (n))).

Similarly, we proceed by coproduct induction, followed by induction on 1 in the left case

and induction on N on the right case, in order to define pinr .

As an application we define the successor function on the integers.

Definition 4.5.4. We define the successor function on the integers succZ : Z → Z using
the induction principle of Lemma 4.5.3, taking

succZ (−1Z ) :≡ 0N
succZ (in-neg(succN (n))) :≡ in-neg(n)
succZ (0Z ) :≡ 1N
succZ (1Z ) :≡ in-pos(1N )
succZ (in-pos(succN (n))) :≡ in-pos(succN (succN (n))).
4. MORE INDUCTIVE TYPES 23

4.6 Dependent pair types

Given a type family B over A, we may consider pairs ( a, b) of terms, where a : A and
b : B( a). Note that the type of b depends on the first term in the pair, so we call such a
pair a dependent pair.
The dependent pair type is an inductive type that is generated by the dependent pairs.
Definition 4.6.1. Consider a type family B over A. The dependent pair type (or Σ-type)
is defined to be the inductive type ∑(x:A) B( x ) equipped with a pairing function
 
( –, – ) : ∏ (x:A) B( x ) → ∑(y:A) B(y) .

The induction principle for ∑(x:A) B( x ) asserts that for any family of types P( p) indexed
by p : ∑(x:A) B( x ), there is a function
   
indΣ : ∏ (x:A) ∏ (y:B(x)) P( x, y) → ∏ ( p:∑(x:A) B(x)) P( p) .

satisfying the computation rule

indΣ ( f , ( x, y)) ≡ f ( x, y).
Sometimes we write λ( x, y). f ( x, y) for indΣ (λx. λy. f ( x, y)).
Definition 4.6.2. Given a type A and a type family B over A, the first projection map
 
pr1 : ∑(x:A) B( x ) → A

is defined by induction as
pr1 :≡ λ( x, y). x.
The second projection map is a dependent function
pr2 : ∏ ( p:∑(x:A) B(x)) B(pr1 ( p))

defined by induction as
pr2 :≡ λ( x, y). y.
By the computation rule we have
pr1 ( x, y) ≡ x
pr2 ( x, y) ≡ y.

4.7 Cartesian products

A special case of the Σ-type occurs when the B is a constant family over A, i.e., when B
is just a type. In this case, the inductive type ∑(x:A) B( x ) is generated by ordinary pairs
( x, y) where x : A and y : B. In other words, if B does not depend on A, then the type
∑(x:A) B is the (cartesian) product A × B. The cartesian product is a very common special
case of the dependent pair type, just as the type A → B of ordinary functions from
A → B is a common special case of the dependent product. Therefore we provide its
specification along with the induction principle for cartesian products.
24 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

Definition 4.7.1. Consider two types A and B. The (cartesian) product of A and B is
defined as the inductive type A × B with constructor

( –, – ) : A → ( B → A × B).

The induction principle for A × B asserts that for any type family P over A × B, one has
   
ind× : ∏ (x:A) ∏ (y:B) P( a, b) → ∏ ( p:A× B) P( p)

satisfying the computation rule that

ind× ( f , ( x, y)) ≡ f ( x, y).

The projection maps are defined similarly to the projection maps of Σ-types. When
one thinks of types as propositions, then A × B is interpreted as the conjunction of A
and B.

Exercises
4.1 Write the rules for 1, ∅, 2, A + B, ∑(x:A) B( x ), and A × B. As usual, present the
rules in four sets:
(i) A formation rule.
(ii) Introduction rules.
(iii) An elimination rule.
(iv) Computation rules.
4.2 Let A be a type.
(a) Show that ( A + ¬ A) → (¬¬ A → A).
(b) Show that ¬¬¬ A → ¬ A.
4.3 Define the following operations of Boolean algebra:

exclusive disjunction p⊕q

implication p⇒q
if and only if p⇔q
Peirce’s arrow (neither . . . nor) p↓q
Sheffer stroke (not both) p | q.

Here p and q range over 2.

4.4 Define the predecessor function predZ : Z → Z.
4.5 Define the group operations

addZ : Z → (Z → Z)
negZ : Z → Z,

and define the multiplication

mulZ : Z → (Z → Z).
4. EXERCISES 25

4.6 Construct a function F : Z → Z that extends the Fibonacci sequence to the negative
integers
. . . , 5, −3, 2, −1, 1, 0, 1, 1, 2, 3, 5, 8, 13, . . .
in the expected way.
4.7 Show that 1 + 1 satisfies the same induction principle as 2, i.e., define

t0 : 1 + 1
t1 : 1 + 1,

and show that for any type family P over 1 + 1 there is a function
 
ind1+1 : P(t0 ) → P(t1 ) → ∏ (t:1+1) P(t)

satisfying

ind1+1 ( p0 , p1 , t0 ) ≡ p0
ind1+1 ( p0 , p1 , t1 ) ≡ p1 .

In other words, type theory cannot distinguish between the types 2 and 1 + 1.
4.8 For any type A we can define the type list( A) of lists elements of A as the inductive
type with constructors

nil : list( A)
cons : A → (list( A) → list( A)).

(a) Write down the induction principle and the computation rules for list( A).
(b) Let A and B be types, suppose that b : B, and consider a binary operation
µ : A → ( B → B). Define a function

fold-list(µ) : list( A) → B

that iterates the operation µ, starting with fold-list(µ, nil) :≡ b.

(c) Define a function length-list : list( A) → N.
(d) Define a function
sum-list : list(N) → N
that adds all the elements in a list of natural numbers.
(e) Define a function

concat-list : list( A) → (list( A) → list( A))

that concatenates any two lists of elements in A.

(f) Define a function

flatten-list : list(list( A)) → list( A)

that concatenates all the lists in a lists of lists in A.

(g) Define a function reverse-list : list( A) → list( A) that reverses the order of the
elements in any list.
26 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

Table I.1: The homotopy interpretation

Type theory Homotopy theory

Types Spaces
Dependent types Fibrations
Terms Points
Dependent pair type Total space
Identity type Path fibration

5 Identity types
From the perspective of types as proof-relevant propositions, how should we think of
equality in type theory? Given a type A, and two terms x, y : A, the equality x = y should
again be a type. Indeed, we want to use type theory to prove equalities. Dependent
type theory provides us with a convenient setting for this: the equality type x = y is
dependent on x, y : A.
Then, if x = y is to be a type, how should we think of the terms of x = y. A term
p : x = y witnesses that x and y are equal terms of type A. In other words p : x = y is an
identification of x and y. In a proof-relevant world, there might be many terms of type
x = y. I.e., there might be many identifications of x and y. And, since x = y is itself a
type, we can form the type p = q for any two identifications p, q : x = y. That is, since
x = y is a type, we may also use the type theory to prove things about identifications (for
instance, that two given such identifications can themselves be identified), and we may
use the type theory to perform constructions with them. As we will see shortly, we can
give every type a groupoidal structure.
Clearly, the equality type should not just be any type dependent on x, y : A. Then
how do we form the equality type, and what ways are there to use identifications in
constructions in type theory? The answer to both these questions is that we will form
the identity type as an inductive type, generated by just a reflexivity term providing
an identification of x to itself. The induction principle then provides us with a way of
performing constructions with identifications, such as concatenating them, inverting
them, and so on. Thus, the identity type is equipped with a reflexivity term, and further
possesses the structure that are generated by its induction principle and by the type
theory. This inductive construction of the identity type is elegant, beautifully simple, but
far from trivial!
The situation where two terms can be identified in possibly more than one way
is analogous to the situation in homotopy theory, where two points of a space can be
connected by possibly more than one path. Indeed, for any two points x, y in a space,
there is a space of paths from x to y. Moreover, between any two paths from x to y there is
a space of homotopies between them, and so on. This leads to the homotopy interpretation
of type theory, outlined in Table I.1. The connection between homotopy theory and type
theory been made precise by the construction of homotopical models of type theory, and
it has led to the fruitful research area of synthetic homotopy theory, the subfield of homotopy
type theory that is the topic of this course.
5. IDENTITY TYPES 27

5.1 The inductive definition of identity types

Definition 5.1.1. Consider a type A and let a : A. Then we define the identity type of A
at a as an inductive family of types a = A x indexed by x : A, of which the constructor is

refla : a = A a.

The induction principle of the identity type postulates that for any family of types P( x, p)
indexed by x : A and p : a = A x, there is a function

path-inda : P( a, refla ) → ∏ (x:A) ∏ ( p:a= A x) P( x, p)

that satisfies path-inda ( p, a, refla ) ≡ p.

A term of type a = A x is also called an identification of a with x, and sometimes it is
called a path from a to x. The induction principle for identity types is sometimes called
identification elimination or path induction. We also write Id A for the identity type on
A, and often we write a = x for the type of identifications of a with x, omitting reference
to the ambient type A.

Remark 5.1.2. We see that the identity type is not just an inductive type, like the inductive
types N, ∅, and 1 for example, but it is and inductive family of types. Even though we
have a type a = A x for any x : A, the constructor only provides a term refla : a = A a,
identifying a with itself. The induction principle then asserts that in order to prove
something about all identifications of a with some x : A, it suffices to prove this assertion
about refla only. We will see in the next sections that this induction principle is strong
enough to derive many familiar facts about equality, namely that it is a symmetric and
transitive relation, and that all functions preserve equality.
Remark 5.1.3. Since the identity types require getting used to, we provide the formal
rules for identity types. The identity type is formed by the formation rule:

Γ`a:A
Γ, x : A ` a = A x type

The constructor of the identity type is then given by the introduction rule:

Γ`a:A
Γ ` refla : a = A a
The induction principle is now given by the elimination rule:

Γ`a:A Γ, x : A, p : a = A x ` P( x, p) type
Γ ` path-inda : P( a, refla ) → ∏ (x:A) ∏ ( p:a= A x) P( x, p)

And finally the computation rule is:

Γ`a:A Γ, x : A, p : a = A x ` P( x, p) type
Γ ` path-inda ( p, a, refla ) ≡ p : P( a, refla )
28 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

Remark 5.1.4. One might wonder whether it is also possible to form the identity type at a
variable of type A, rather than at a term. This is certainly possible: since we can form the
identity type in any context, we can form the identity type at a variable x : A as follows:

Γ, x : A ` x : A
Γ, x : A, y : A ` x = A y type

In this way we obtain the ‘binary’ identity type. Its constructor is then also indexed by
x : A. We have the following introduction rule

Γ, x : A ` x : A
Γ, x : A ` reflx : x = A x

and similarly we have elimination and computation rules.

5.2 The groupoidal structure of types

We show that identifications can be concatenated and inverted, which corresponds to the
transitivity and symmetry of the identity type.

Definition 5.2.1. Let A be a type. We define the concatenation operation

concat : ∏ (x,y,z:A) ( x = y) → (y = z) → ( x = z).

We will write p  q for concat( p, q).

Construction. We construct the concatenation operation by path induction. It suffices to

construct
concat(reflx ) : ∏ (z:A) ( x = z) → ( x = z).
Here we take concat(reflx )z ≡ id(x=z) . Explicitly, the term we have constructed is

λx. path-indx (λz. id(x= z) ) : ∏ (x,y:A) ( x = y) → ∏ (z:A) (y = z) → ( x = z).

To obtain a term of the asserted type we need to swap the order of the arguments
p : x = y and z : A, using Exercise 2.5.

Definition 5.2.2. Let A be a type. We define the inverse operation

inv : ∏ (x,y:A) ( x = y) → (y = x ).

Most of the time we will write p−1 for inv( p).

Construction. We construct the inverse operation by path induction. It suffices to con-

struct
inv(reflx ) : x = x,
for any x : A. Here we take inv(reflx ) :≡ reflx .
5. IDENTITY TYPES 29

The next question is whether the concatenation and inverting operations on paths
behave as expected. More concretely, is path concatenation associative, does it satisfy
the unit laws, and is the inverse of a path indeed a two-sided inverse?
For example, in the case of associativity we are asking to compare the paths
( p  q)  r and p  (q  r )
for any p : x = y, q : y = z, and r : z = w in a type A. The computation rules of path
induction are not strong enough to conclude that ( p  q)  r and p  (q  r ) are judgmentally
equal. However, both ( p  q)  r and p  (q  r ) are terms of the same type: they are
identifications of type x = w. Since the identity type is a type like any other, we can ask
whether there is an identification
( p  q )  r = p  ( q  r ).
This is a very useful idea: while it is often impossible to show that two terms of the same
type are judgmentally equal, it may be the case that those two terms can be identified.
Indeed, we identify two terms by constructing a term of the identity type, and we can use
all the type theory at our disposal in order to construct such a term. In this way we can
show, for example, that addition on the natural numbers or on the integers is associative
and satisfies the unit laws. And indeed, here we will show that path concatenation is
associative and satisfies the unit laws.
Definition 5.2.3. Let A be a type and consider three consecutive paths
p q r
x y z w

in A. We define the associator

assoc( p, q, r ) : ( p  q)  r = p  (q  r ).
Construction. By path induction it suffices to show that
∏ (z:A) ∏ (q:x=z) ∏ (w:A) ∏ (r:z=w) (reflx  q)  r = reflx  (q  r ).
Let q : x = z and r : z = w. Note that by the computation rule of the path induction
principle we have a judgmental equality reflx  q ≡ q. Therefore we conclude that
(reflx  q)  r ≡ q  r.
Similarly we have a judgmental equality reflx  (q  r ) ≡ q  r. Thus we see that the
left-hand side and the right-hand side in
(reflx  q)  r = reflx  (q  r )
are judgmentally equal, so we can simply define assoc(reflx , q, r ) :≡ reflq  r .
Definition 5.2.4. Let A be a type. We define the left and right unit law operations,
which assigns to each p : x = y the terms
left-unit( p) : reflx  p = p
right-unit( p) : p  refly = p,
respectively.
30 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

Construction. By identification elimination it suffices to construct

left-unit(reflx ) : reflx  reflx = reflx
right-unit(reflx ) : reflx  reflx = reflx .
In both cases we take reflreflx .
Definition 5.2.5. Let A be a type. We define left and right inverse law operations
left-inv( p) : p−1  p = refly
right-inv( p) : p  p−1 = reflx .
Construction. By identification elimination it suffices to construct
left-inv(reflx ) : refl−
x
1
reflx = reflx
right-inv(reflx ) : reflx  refl− 1
x = reflx .

Using the computation rules we see that

refl−
x
1
reflx ≡ reflx  reflx ≡ reflx ,
so we define left-inv(reflx ) :≡ reflreflx . Similarly it follows from the computation rules that
reflx  refl− 1 −1
x ≡ reflx ≡ reflx

so we again define right-inv(reflx ) :≡ reflreflx .

Remark 5.2.6. We have seen that the associator, the unit laws, and the inverse laws, are
all proven by constructing an identification of identifications. And indeed, there is
nothing that would stop us from considering identifications of those identifications of
identifications. We can go up as far as we like in the tower of identity types, which is
obtained by iteratively taking identity types.
The iterated identity types give types in homotopy type theory a very intricate
structure. One important way of studying this structure is via the homotopy groups of
types, a subject that we will gradually be working towards.

5.3 The action on paths of functions

Using the induction principle of the identity type we can show that every function
preserves identifications. In other words, every function sends identified terms to
identified terms. Note that this is a form of continuity for functions in type theory: if
there is a path that identifies two points x and y of a type A, then there also is a path that
identifies the values f ( x ) and f (y) in the codomain of f .
Definition 5.3.1. Let f : A → B be a map. We define the action on paths of f as an
operation
ap f : ∏ (x,y:A) ( x = y) → ( f ( x ) = f (y)).
Moreover, there are operations
ap-id A : ∏ (x,y:A) ∏ ( p:x= y) p = apid A ( p)
ap-comp( f , g) : ∏ (x,y:A) ∏ ( p:x= y) apg (ap f ( p)) = apg◦ f ( p).
5. IDENTITY TYPES 31

Construction. First we define ap f by identity elimination, taking

ap f (reflx ) :≡ refl f (x) .

Next, we construct ap-id A by identity elimination, taking

ap-id A (reflx ) :≡ reflreflx .

Finally, we construct ap-comp( f , g) by identity elimination, taking

ap-comp( f , g, reflx ) :≡ reflg( f (x)) .

Definition 5.3.2. Let f : A → B be a map. Then there are identifications

ap-refl( f , x ) : ap f (reflx ) = refl f ( x )

ap-inv( f , p) : ap f ( p−1 ) = ap f ( p)−1
ap-concat( f , p, q) : ap f ( p  q) = ap f ( p)  ap f (q)

for every p : x = y and q : x = y.

Construction. To construct ap-refl( f , x ) we simply observe that ap f (reflx ) ≡ refl f ( x ), so

we take
ap-refl( f , x ) :≡ reflrefl f (x) .

We construct ap-inv( f , p) by identification elimination on p, taking

ap-inv( f , reflx ) :≡ reflap f (reflx ) .

Finally we construct ap-concat( f , p, q) by identification elimination on p, taking

ap-concat( f , reflx , q) :≡ reflap f (q) .

5.4 Transport
Dependent types also come with an action on paths: the transport functions. Given an
identification p : x = y in the base type A, we can transport any term b : B( x ) to the
fiber B(y). The transport functions have many applications, which we will encounter
throughout this course.

Definition 5.4.1. Let A be a type, and let B be a type family over A. We will construct a
transport operation

tr B : ∏ (x,y:A) ( x = y) → ( B( x ) → B(y)).

Construction. We construct tr B ( p) by induction on p : x = A y, taking

tr B (reflx ) :≡ idB(x) .
32 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

Thus we see that type theory cannot distinguish between identified terms x and y,
because for any type family B over A one gets a term of B(y) as soon as B( x ) has a term.
As an application of the transport function we construct the dependent action on paths
of a dependent function f : ∏ (x:A) B( x ). Note that for such a dependent function f ,
and an identification p : x = A y, it does not make sense to directly compare f ( x ) and
f (y), since the type of f ( x ) is B( x ) whereas the type of f (y) is B(y), which might not be
exactly the same type. However, we can first transport f ( x ) along p, so that we obtain
the term tr B ( p, f ( x )) which is of type B(y). Now we can ask whether it is the case that
tr B ( p, f ( x )) = f (y). The dependent action on paths of f establishes this identification.

Definition 5.4.2. Given a dependent function f : ∏ (a:A) B( a) and a path p : x = y in A,

we construct a path
apd f ( p) : tr B ( p, f ( x )) = f (y).

Construction. The path apd f ( p) is constructed by path induction on p. Thus, it suffices

to construct a path
apd f (reflx ) : tr B (reflx , f ( x )) = f ( x ).
Since transporting along reflx is the identity function on B( x ), we simply take apd f (reflx ) :≡
refl f (x) .

Exercises
5.1 (a) State Goldbach’s Conjecture in type theory.
(b) State the Twin Prime Conjecture in type theory.
5.2 Show that the operation inverting paths distributes over the concatenation opera-
tion, i.e., construct an identification

distributive-inv-concat( p, q) : ( p  q)−1 = q−1  p−1 .

for any p : x = y and q : y = z.

5.3 For any p : x = y, q : y = z, and r : x = z, construct maps

inv-con( p, q, r ) : ( p  q = r ) → (q = p−1  r )
con-inv( p, q, r ) : ( p  q = r ) → ( p = r  q−1 ).

5.4 Let B be a type family over A, and consider a path p : x = x 0 in A. Construct for
any y : B( x ) a path
liftB ( p, y) : ( x, y) = ( x 0 , tr B ( p, y)).
In other words, a path in the base type A lifts to a path in the total space ∑(x:A) B( x )
for every term over the domain, analogous to the path lifting property for fibrations
in homotopy theory.
5.5 Show that the operations of addition and multiplication on the natural numbers
satisfy the laws of a commutative semi-ring:

m + (n + k) = (m + n) + k m · (n · k) = (m · n) · k
m+0 = m m·1 = m
0+m = m 1·m = m
6. TYPE THEORETIC UNIVERSES 33

m+n = n+m m·0 = 0

0·m = 0
m·n = n·m
m · (n + k ) = m · n + m · k.

5.6 Consider four consecutive identifications

p q r s
a b c d e

in a type A. In this exercise we will show that the Mac Lane pentagon for identifi-
cations commutes.
(a) Construct the five identifications α1 , . . . , α5 in the pentagon
α4
(( p  q)  r )  s ( p  q )  (r  s )
α1 α5

( p  (q  r ))  s p  (q  (r  s)),

α2 α3

p  ((q  r )  s)

where α1 , α2 , and α3 run counter-clockwise, and α4 and α5 run clockwise.

(b) Show that
( α1  α2 )  α3 = α4  α5 .

6 Type theoretic universes

To complete our specification of dependent type theory, we introduce type theoretic
universes. Universes are types that consist of types. In other words, a universe is a type
U that comes equipped with a type family T over U , and for any X : U we think of X as
an encoding of the type T ( X ). We call this type family the universal type family.
There are several reasons to equip type theory with universes. One reason is that
it enables us to define new type families over inductive types, using their induction
principle. For example, since the universe is itself a type, we can use the induction
principle of 2 to obtain a map P : 2 → U from any two terms X0 , X1 : U . Then we obtain
a type family over 2 by substituting P into the universal type family:

x : 2 ` T ( P( x )) type

satisfying T ( P(02 )) ≡ T ( X0 ) and T ( P(12 )) ≡ T ( X1 ).

We use this way of defining type families to define many familiar relations over
N, such as ≤ and <. We also introduce a relation called observational equality EqN on
N, which we can think of as equality of N. This relation is reflexive, symmetric, and
transitive, and moreover it is the least reflexive relation. Furthermore, one of the most
important aspects of observational equality EqN on N is that EqN (m, n) is a type for
34 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

every m, n : N, unlike judgmental equality. Therefore we can use type theory to reason
about observational equality on N. Indeed, in the exercises we show that some very
elementary mathematics can already be done at this early stage in our development of
type theory.
A second reason to introduce universes is that it allows us to define many types
of types equipped with structure. One of the most important examples is the type of
groups, which is the type of types equipped with the group operations satisfying the
group laws, and for which the underlying type is a set. We won’t discuss the condition
for a type to be a set until §10, so the definition of groups in type theory will be given
much later. Therefore we illustrate this use of the universe by giving simpler examples:
pointed types, graphs, and reflexive graphs.
One of the aspects that make universes useful is that they are postulated to be closed
under all the type constructors. For example, if we are given X : U and P : T ( X ) → U ,
then the universe is equipped with a term
Σ̌( X, P) : U
satisfying the judgmental equality T (Σ̌( X, P) ≡ ∑(x:T (X )) T ( P( x )). We will similarly
assume that any universe is closed under Π-types and the other ways of forming types.
However, there is an important restriction: it would be inconsistent to assume that the
universe is contained in itself. One way of thinking about this is that universes are types
of small types, and it cannot be the case that the universe is small with respect to itself.
We address this problem by assuming that there are many universes: enough universes
so that any type family can be obtained by substituting into the universal type family of
some universe.

6.1 Specification of type theoretic universes

In the following definition we already state that universes are closed under identity
types. Identity types will be introduced in §5.
Definition 6.1.1. A universe in type theory is a closed type U equipped with a type
family T over U called the universal family, equipped with the following structure:
(i) U is closed under Π, in the sense that it comes equipped with a function
Π̌ : ∏ (X:U ) (T ( X ) → U ) → U
for which the judgmental equality
T Π̌( X, P) ≡ ∏ (x:T (X )) T ( P( x )).

holds, for every X : U and P : T ( X ) → U .

(ii) U is closed under Σ in the sense that it comes equipped with a function
Σ̌ : ∏ (X:U ) (T ( X ) → U ) → U
for which the judgmental equality
T Σ̌( X, P) ≡ ∑(x:T (X )) T ( P( x ))

holds, for every X : U and P : T ( X ) → U .

6. TYPE THEORETIC UNIVERSES 35

(iii) U is closed under identity types, in the sense that it comes equipped with a function

Ǐ : ∏ (X:U ) T ( X ) → (T ( X ) → U )

for which the judgmental equality

T Ǐ( X, x, y) ≡ ( x = y)

holds, for every X : U and x, y : T ( X ).

(iv) U is closed under coproducts, in the sense that it comes equipped with a function

+̌ : U → (U → U )


that satisfies T X +̌Y ≡ T ( X ) + T (Y ).
ˇ 1̌, Ň : U that satisfy the judgmental equalities
(v) U contains terms ∅,

T ∅ ˇ ≡∅




T 1̌ ≡ 1
T (Ň) ≡ N.

Given a universe U , we say that a type A in context Γ is small with respect to U if it

occurs in the universe, i.e., if it comes equipped with a term Ǎ : U in context Γ, for which
the judgment
Γ ` T Ǎ ≡ A type

holds. If A is small with respect to U , we usually write simply A for Ǎ and also A for
T ( Ǎ). In other words, by A : U we mean that A is a small type.
Remark 6.1.2. Since ordinary function types are defined as a special case of dependent
function types, we don’t have to assume that universes are closed under ordinary
function types. Similarly, it follows from the assumption that universes are closed under
dependent pair types that universes are closed under cartesian product types.

6.2 Assuming enough universes

Most of the time we will get by with assuming one universe U , and indeed we rec-
ommend on a first reading of this text to simply assume that there is one universe U .
However, sometimes we might need a second universe V that contains U as well as
all the types in U . In such situations we cannot get by with a single universe, because
the assumption that U is a term of itself would lead to inconsistencies like the Russel’s
paradox.
Russel’s paradox is the famous argument that there cannot be a set of all sets. If there
were such a set S, then we could consider Russel’s subset

R := { x ∈ S | x ∈
/ x }.

Russell then observed that R ∈ R if and only if R ∈ / R, so we reach a contradiction.

A variant of this argument reaches a similar contradiction when we assume that U is
36 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

a universe that contains a term Ǔ : U such that T Ǔ ≡ U . In order to avoid such
paradoxes, Russell and Whitehead formulated the ramified theory of types in their book
Principia Mathematica. The ramified theory of types is a precursor of Martin Löf’s type
theory that we are studying in this course.
Even though the universe is not a term of itself, it is still convenient if every type,
including any universe, is small with respect to some universe. Therefore we will assume
that there are sufficiently many universes: we will assume that for every finite list of
types

Γ1 ` A1 type
..
.

Γn ` An type,

there is a universe U that contains each Ai in the sense that U comes equipped with a
term

Γi ` Ǎi : U

for which the judgment

Γi ` T Ǎi ≡ Ai type

holds. With this assumption it will rarely be necessary to work with more than one
universe at the same time.
Remark 6.2.1. Using the assumption that for any finite list of types in context there is a
universe that contains those types, we obtain many specific universes:

(i) There is a base universe U0 that we obtain using the empty list of types in context.
This is a universe, but it isn’t specified to contain any further types.

(ii) Given a finite list

Γ1 ` A1 type
..
.

Γn ` An type,

of types in context, and a universe U that contains them, there is a universe U +

that contains all the types in U as well as U . More precisely, it is specified by the
finite list

` U type
X : U ` T ( X ) type.

Note that since the universe U + contains all the types in U , it also contains the
types A1 , . . . , An . To see this, we derive that there is a code for Ai in U + .
6. TYPE THEORETIC UNIVERSES 37

X : U ` Ť ( X ) : U +
Γi ` Ǎi : U Γi , X : U ` Ť ( X ) : U +
Γi ` Ť ( Ǎi ) : U +

We leave it as an exercise to derive the judgmental equality

T + (Ť ( Ǎi )) ≡ Ai .

(iii) Given two finite lists

Γ1 ` A1 type ∆1 ` B1 type
.. ..
. .

Γn ` An type ∆m ` Bm type

of types in context, and two universes U and V that contain A1 , . . . , An and

B1 , . . . , Bm respectively, there is a universe U t V that contains the types of both U
and V . The universe U t V is specified by the finite list

X : U ` TU ( X ) type
Y : V ` TV (Y ) type.

With an argument similar to the previous construction of a universe, we see that

the universe U t V contains the types A1 , . . . , An as well as the types B1 , . . . , Bm .
Note that we could also directly obtain a universe W that contains the types
A1 , . . . , An and B1 , . . . , Bm . However, this universe might not contain all the types
in U or all the types in V .

Since we don’t postulate any relations between the universes, there are indeed very few
of them. For example, the base universe U0 might contain many more types than it is
postulated to contain. Nevertheless, there are some relations between the universes. For
instance, there is a function U → U + , since we can simply derive

X : U ` Ť ( X ) : U +
` λX. Ť ( X ) : U → U +
Similarly, there are functions U → U t V and V → U t V for any two universes U and
V.

6.3 Pointed types

Definition 6.3.1. A pointed type is a pair ( A, a) consisting of a type A and a term a : A.
The type of all pointed types in a universe U is defined to be

U∗ :≡ ∑(X:U ) X.
38 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

Definition 6.3.2. Consider two pointed types ( A, a) and ( B, b). A pointed map from
( A, a) to ( B, b) is a pair ( f , p) consisting of a function f : A → B and an identification
p : f ( a) = b. We write
A →∗ B :≡ ∑( f :A→ B) f ( a) = b
for the type of all pointed maps from ( A, a) to ( B, b), leaving the base point implicit.

Since we have a type U∗ of all pointed types in a universe U , we can start defining
operations on U∗ . An important example of such an operation is to take the loop space
of a pointed type.

Definition 6.3.3. We define the loop space operation Ω : U∗ → U∗

Ω( A, a) :≡ ( a = a), refla .

We can even go further and define the iterated loop space of a pointed type. Note that
this definition could not be given in type theory if we didn’t have universes.

Definition 6.3.4. Given a pointed type ( A, a) and a natural number n, we define the n-th
loop space Ωn ( A, a) by induction on n : N, taking

Ω0 ( A, a) :≡ ( A, a)
Ωn+1 ( A, a) :≡ Ω(Ωn ( A, a)).

6.4 Families and relations on the natural numbers

As we have already seen in the case of the iterated loop space, we can use the universe
to define a type family over N by induction on N. For example, we can define the finite
types in this way.

Definition 6.4.1. We define the type family Fin : N → U of finite types by induction on
N, taking

Fin(0N ) :≡ ∅
Fin(succN (n)) :≡ Fin(n) + 1

Similarly, we can define many relations on the natural numbers using a universe. We
give here the example of observational equality on N. This inductively defined equivalence
relation is very important, as it can be used to show that equality on the natural numbers
is decidable, i.e., there is a program that decides for any two natural numbers m and n
whether they are equal or not.

Definition 6.4.2. We define the observational equality on N as binary relation EqN :

N → (N → U ) satisfying

EqN (0N , 0N ) ≡ 1 EqN (succN (n), 0N ) ≡ ∅

EqN (0N , succN (n)) ≡ ∅ EqN (succN (n), succN (m)) ≡ EqN (n, m).
6. TYPE THEORETIC UNIVERSES 39

Construction. We define EqN by double induction on N. By the first application of

induction it suffices to provide

E0 : N → U
ES : N → (N → U ) → (N → U )
We define E0 by induction, taking E00 :≡ 1 and E0S (n, X, m) :≡ ∅. The resulting family
E0 satisfies

E0 (0N ) ≡ 1
E0 (succN (n)) ≡ ∅.
We define ES by induction, taking ES0 :≡ ∅ and ES0 (n, X, m) :≡ X (m). The resulting
family ES satisfies

ES (n, X, 0N ) ≡ ∅
ES (n, X, succN (m)) ≡ X (m)
Therefore we have by the computation rule for the first induction that the judgmental
equality

EqN (0N , m) ≡ E0 (m)

EqN (succN (n), m) ≡ ES (n, EqN (n), m)
holds, from which the judgmental equalities in the statement of the definition follow.
Lemma 6.4.3. Suppose R : N → (N → U ) is a reflexive relation on N, i.e., R comes equipped
with
ρ : ∏ (n:N) R(n, n).
Then there is a family of maps
∏ (m,n:N) EqN (m, n) → R(m, n).
Proof. We will prove by induction on m, n : N that there is a term of type
 
f m,n : ∏ (e:EqN (m,n)) ∏ ( R:N→(N→U )) ∏ (x:N) R( x, x ) → R(m, n)

The dependent function f m,n is defined by

f 0N ,0N :≡ λ ? . λr. λρ. ρ(0N )

f 0N ,succN (n) :≡ ind∅
f succN (m),0N :≡ ind∅
f succN (m),succN (n) :≡ λe. λR. λρ. f m,n (e, R0 , ρ0 ),
where R0 and ρ0 are given by

R0 (m, n) :≡ R(succN (m), succN (n))

ρ0 (n) :≡ ρ(succN (n)).
40 CHAPTER I. MARTIN-LÖF’S DEPENDENT TYPE THEORY

We can also define observational equality for many other kinds of types, such as 2 or
Z. In each of these cases, what sets the observational equality apart from other relations
is that it is the least reflexive relation.

Exercises
6.1 Show that observational equality on N is an equivalence relation, i.e., construct
terms of the following types:

∏ (n:N) EqN (n, n)

∏ (n,m:N) EqN (n, m) → EqN (m, n)
∏ (n,m,l:N) EqN (n, m) → (EqN (m, l ) → EqN (n, l )).
6.2 Let R be a reflexive binary relation on N, i.e., R is of type N → (N → U ) and
comes equipped with a term ρ : ∏ (n:N) R(n, n). Show that
∏ (n,m:N) EqN (n, m) → R(n, m).
6.3 Show that every function f : N → N preserves observational equality in the sense
that
∏ (n,m:N) EqN (n, m) → EqN ( f (n), f (m)).
Hint: to get the inductive step going the induction hypothesis has to be strong enough.
Construct by double induction a term of type
∏ (n,m:N) ∏ ( f :N→N) EqN (n, m) → EqN ( f (n), f (m)),
and pull out the universal quantification over f : N → N by Exercise 2.5.
6.4 (a) Define the order relations ≤ and < on N.
(b) Show that ≤ is reflexive and that < is anti-reflexive, i.e., that ¬(n < n).
(c) Show that both ≤ and < are transitive, and that n < S(n).
(d) Show that k ≤ min(m, n) holds if and only if both k ≤ m and k ≤ n hold, and
show that max(m, n) ≤ k holds if and only if both m ≤ k and n ≤ k hold.
6.5 (a) Define observational equality Eq2 on the booleans.
(b) Show that Eq2 is reflexive.
(c) Show that for any reflexive relation R : 2 → (2 → U ) one has
∏ (x,y:2) Eq2 ( x, y) → R( x, y).
6.6 (a) Define the order relations ≤ and < on and Z.
(b) Show that ≤ is reflexive, transitive, and anti-symmetric.
(c) Show that < is anti-reflexive and transitive.
6.7 (a) Show that N satisfies strong induction, i.e., construct for any type family P
over N a function of type
   
P(0N ) → ∏ (k:N) ∏ (m:N) (m ≤ k) → P(m) → P(succN (k )) → ∏ (n:N) P(n).

(b) Show that N satisfies ordinal induction, i.e., construct for any type family P
over N a function of type
   
∏ (k:N) ∏ (m:N) (m < k ) → P(m) → P(k ) → ∏ (n:N) P(n).
Chapter II

Basic concepts of type theory

7 Equivalences
7.1 Homotopies
In homotopy type theory, a homotopy is just a pointwise equality between two functions
f and g. We view the type of homotopies as the observational equality for Π-types.

Definition 7.1.1. Let f , g : ∏ (x:A) P( x ) be two dependent functions. The type of homo-
topies from f to g is defined as

f ∼ g :≡ ∏ (x:A) f ( x ) = g( x ).

Note that the type of homotopies f ∼ g is a special case of a dependent function

type. Therefore the definition of homotopies is set up in such a way that we may also
consider homotopies between homotopies, and even further homotopies between those
higher homotopies. More concretely, if H, K : f ∼ g are two homotopies, then the type
of homotopies H ∼ K between them is just the type

∏ (x:A) H ( x ) = K ( x ).

In the following definition we define the groupoidal structure of homotopies. Note

that we implement the groupoid laws as homotopies rather than as identifications.

Definition 7.1.2. For any type family B over A there are operations

htpy-refl : ∏ ( f :∏ (x:A) B(x)) f ∼ f

htpy-inv : ∏ ( f ,g:∏ (x:A) B(x)) ( f ∼ g) → ( g ∼ f )

htpy-concat : ∏ ( f ,g,h:∏ (x:A) B(x)) ( f ∼ g) → (( g ∼ h) → ( f ∼ h)).

We will write H −1 for htpy-inv( H ), and H  K for htpy-concat( H, K ).

Furthermore, we define

htpy-assoc( H, K, L) : ( H  K )  L ∼ H  (K  L)
htpy-left-unit( H ) : htpy-refl f  H ∼ H

41
42 CHAPTER II. BASIC CONCEPTS OF TYPE THEORY

htpy-right-unit( H ) : H  htpy-reflg ∼ H
htpy-left-inv( H ) : H −1  H ∼ htpy-reflg
htpy-right-inv( H ) : H  H −1 ∼ htpy-refl f
for any H : f ∼ g, K : g ∼ h and L : h ∼ i, where f , g, h, i : ∏ (x:A) B( x ).
Construction. We define
htpy-refl( f ) :≡ λx. refl f (x)
htpy-inv( H ) :≡ λx. H ( x )−1
htpy-concat( H, K ) :≡ λx. H ( x )  K ( x ),
where H : f ∼ g and K : g ∼ h are homotopies. Furthermore, we define

htpy-assoc( H, K, L) :≡ λx. assoc( H ( x ), K ( x ), L( x ))

htpy-left-unit( H ) :≡ λx. left-unit( H ( x ))
htpy-right-unit( H ) :≡ λx. right-unit( H ( x ))
htpy-left-inv( H ) :≡ λx. left-inv( H ( x ))
htpy-right-inv(h) :≡ λx. right-inv( H ( x )).
Apart from the groupoid operations and their laws, we will occasionally need whisker-
ing operations.
Definition 7.1.3. We define the following whiskering operations on homotopies:
(i) Suppose H : f ∼ g for two functions f , g : A → B, and let h : B → C. We define
h · H :≡ λx. aph ( H ( x )) : h ◦ f ∼ h ◦ g.

(ii) Suppose f : A → B and H : g ∼ h for two functions g, h : B → C. We define

H · f :≡ λx. H ( f ( x )) : h ◦ f ∼ g ◦ f .

We also use homotopies to express the commutativity of diagrams. For example, we

say that a triangle
h
A B

f g
X
commutes if it comes equipped with a homotopy H : f ∼ g ◦ h, and we say that a square
g
A A0
f f0

B B0
h

if it comes equipped with a homotopy h ◦ f g ◦ f 0 .

7. EQUIVALENCES 43

7.2 Bi-invertible maps

Definition 7.2.1. Let f : A → B be a function. We say that f has a section if there is a
term of type
sec( f ) :≡ ∑( g:B→ A) f ◦ g ∼ idB .
Dually, we say that f has a retraction if there is a term of type

retr( f ) :≡ ∑(h:B→ A) h ◦ f ∼ id A .

If a map f : A → B has a retraction, we also say that A is a retract of B. We say that a

function f : A → B is an equivalence if it has both a section and a retraction, i.e., if it
comes equipped with a term of type

is-equiv( f ) :≡ sec( f ) × retr( f ).

We will write A ' B for the type ∑( f :A→ B) is-equiv( f ).

Remark 7.2.2. An equivalence, as we defined it here, can be thought of as a bi-invertible

map, since it comes equipped with a separate left and right inverse. Explicitly, if f is an
equivalence, then there are

g:B→A h:B→A
G : f ◦ g ∼ idB H : h ◦ f ∼ id A .

Clearly, if f has an inverse in the sense that it comes equipped with a function g : B → A
such that f ◦ g ∼ idB and g ◦ f ∼ id A , then f is an equivalence. We write

has-inverse( f ) :≡ ∑( g:B→ A) ( f ◦ g ∼ idB ) × ( g ◦ f ∼ id A ).

Lemma 7.2.3. Any equivalence e : A ' B can be given the structure of an invertible map. We
define e−1 to be the section g : B → A of e.

Proof. First we construct for any equivalence f with right inverse g and left inverse h a
homotopy K : g ∼ h. For any y : B, we have

H ( g(y))−1 aph ( G (y))

g(y) h f g(y) h ( y ).

Therefore we define a homotopy K : g ∼ h by K :≡ ( H · g)−1  h · G. Using the homotopy

K we are able to show that g is also a left inverse of f . For x : A we have the identification

K ( f ( x )) H (x)
g f (x) h f (x) x.

Corollary 7.2.4. The inverse of an equivalence is again an equivalence.

Proof. Let f : A → B be an equivalence. By Lemma 7.2.3 it follows that the section of f

is also a retraction. Therefore it follows that the section is itself an invertible map, with
inverse f . Hence it is an equivalence.
44 CHAPTER II. BASIC CONCEPTS OF TYPE THEORY

Remark 7.2.5. For any type A, the identity function id A is an equivalence, since it is its
own section and its own retraction
Example 7.2.6. For any type C ( x, y) indexed by x : A and y : B, the swap function
   
σ : ∏ (x:A) ∏ (y:B) C ( x, y) → ∏ (y:B) ∏ (x:A) C ( x, y)

that swaps the order of the arguments x and y is an equivalence by Exercise 2.5.

7.3 The identity type of a Σ-type

In this section we characterize the identity type of a Σ-type as a Σ-type of identity types.
In this course we will be characterizing the identity types of many types, so we will
follow the general outline of how such a characterization goes:

(i) First we define a binary relation R : A → A → U on the type A that we are

interested in. This binary relation is intended to be equivalent to its identity type.

(ii) Then we will show that this binary relation is reflexive, by constructing a term of
type
∏ (x:A) R( x, x )

(iii) Using the reflexivity we will show that there is a canonical map

( x = y) → R( x, y)

for every x, y : A. This map is just constructed by path induction, using the
reflexivity of R.

(iv) Finally, it has to be shown that the map

( x = y) → R( x, y)

is an equivalence for each x, y : A.

The last step is usually the most difficult, and we will refine our methods for this step in
§9, where we establish the fundamental theorem of identity types.
In this section we consider a type family B over A. Given two pairs

( x, y), ( x 0 , y0 ) : ∑(x:A) B( x ),

if we have a path α : x = x 0 then we can compare y : B( x ) to y0 : B( x 0 ) by first

transporting y along α, i.e., we consider the identity type

tr B (α, y) = y0 .

Thus it makes sense to think of ( x, y) to be identical to ( x 0 , y0 ) if there is an identification

α : x = x 0 and an identification β : tr B (α, y) = y0 . In the following definition we turn this
idea into a binary relation on the Σ-type.
7. EQUIVALENCES 45

Definition 7.3.1. We will define a relation

   
EqΣ : ∑(x:A) B( x ) → ∑(x:A) B( x ) → U

by defining
EqΣ (s, t) :≡ ∑(α:pr1 (s)=pr1 (t)) tr B (α, pr2 (s)) = pr2 (t).

Lemma 7.3.2. The relation EqΣ is reflexive, i.e., there is a term

reflexive-EqΣ : ∏ (s:∑(x:A) B(x)) EqΣ (s, s).

Construction. This term is constructed by Σ-induction on s : ∑(x:A) B( x ). Thus, it suffices

to construct a term of type

∏ (x:A) ∏ (y:B(x)) ∑(α:x= x) tr B (α, y) = y.

Here we take λx. λy. (reflx , refly ).

Definition 7.3.3. Consider a type family B over A. Then for any s, t : ∑(x:A) B( x ) we
define a map
pair-eq : (s = t) → EqΣ (s, t)
by path induction, taking pair-eq(refls ) :≡ reflexive-EqΣ (s).

Theorem 7.3.4. Let B be a type family over A. Then the map

pair-eq : (s = t) → EqΣ (s, t)

is an equivalence for every s, t : ∑(x:A) B( x ).

Proof. The maps in the converse direction

eq-pair : EqΣ (s, t) → (s = t)

are defined by repeated Σ-induction. By Σ-induction on s and t we see that it suffices to

define a map
 
eq-pair : ∑( p:x= x0 ) tr B ( p, y) = y0 → (( x, y) = ( x 0 , y0 )).

A map of this type is again defined by Σ-induction. Thus it suffices to define a dependent
function of type
∏ ( p:x= x0 ) (tr B ( p, y) = y0 ) → (( x, y) = ( x 0 , y0 )).
Such a dependent function is defined by double path induction by sending (reflx , refly )
to refl(x,y) . This completes the definition of the function eq-pair.
Next, we must show that eq-pair is a section of pair-eq. In other words, we must
construct an identification

pair-eq(eq-pair(α, β)) = (α, β)

46 CHAPTER II. BASIC CONCEPTS OF TYPE THEORY

for each (α, β) : ∑(α:x= x0 ) tr B (α, y) = y0 . We proceed by path induction on α, followed by

path induction on β. Then our goal becomes to construct a term of type

pair-eq(eq-pair(reflx , refly )) = (reflx , refly )

By the definition of eq-pair we have eq-pair(reflx , refly ) ≡ refl(x,y) , and by the definition
of pair-eq we have pair-eq(refl(x,y) ) ≡ (reflx , refly ). Thus we may take refl(reflx ,refly ) to
complete the construction of the homotopy pair-eq ◦ eq-pair ∼ id.
To complete the proof, we must show that eq-pair is a retraction of pair-eq. In other
words, we must construct an identification

eq-pair(pair-eq( p)) = p

for each p : s = t. We proceed by path induction on p : s = t, so it suffices to construct

an identification
eq-pair(reflpr1 (s) , reflpr2 (s) ) = refls .
Now we proceed by Σ-induction on s : ∑(x:A) B( x ), so it suffices to construct an identifi-
cation
eq-pair(reflx , refly ) = refl(x,y) .
Since eq-pair(reflx , refly ) computes to refl(x,y) , we may simply take reflrefl(x,y) .

Exercises
7.1 Show that the functions

inv : ( x = y) → (y = x )
concat( p) : (y = z) → ( x = z)
concat0 (q) : ( x = y) → ( x = z)
tr B ( p) : B( x ) → B(y)

are equivalences, where concat0 (q, p) :≡ p  q. Give their inverses explicitly.

7.2 Show that the maps

inl : X → X + ∅ pr1 : ∅ × X → ∅
inr : X → ∅ + X pr2 : X × ∅ → ∅

are equivalences.
7.3 (a) Consider two functions f , g : A → B and a homotopy H : f ∼ g. Then

is-equiv( f ) ↔ is-equiv( g).

(b) Show that for any two homotopic equivalences e, e0 : A ' B, their inverses
are also homotopic.
7. EXERCISES 47

7.4 Consider a commuting triangle

h
A B

f g
X.
with H : f ∼ g ◦ h.
(a) Suppose that the map h has a section s : B → A. Show that the triangle
s
B A
g f
X.
commutes, and that f has a section if and only if g has a section.
(b) Suppose that the map g has a retraction r : X → B. Show that the triangle
f
A X

h r
B.
commutes, and that f has a retraction if and only if h has a retraction.
(c) (The 3-for-2 property for equivalences.) Show that if any two of the functions
f, g, h
are equivalences, then so is the third.
7.5 (a) Show that the negation function on the booleans neg2 : 2 → 2 defined in
Example 4.4.2 is an equivalence.
(b) Use the observational equality on the booleans, defined in Exercise 6.5, to
show that 02 6= 12 .
(c) Show that for any b : 2, the constant function constb is not an equivalence.
7.6 Show that the successor function on the integers is an equivalence.
7.7 Construct a equivalences A + B ' B + A and A × B ' B × A.
7.8 Consider a section-retraction pair
i r
A B A,

with H : r ◦ i ∼ id. Show that x = y is a retract of i ( x ) = i (y).

7.9 Let B be a family of types over A, and let C be a family of types indexed by
x : A, y : B( x ). Construct an equivalence
   
assoc-Σ : ∑( p:∑(x:A) B(x)) C (pr1 ( p), pr2 ( p)) ' ∑(x:A) ∑(y:B(x)) C ( x, y) .

7.10 Let A and B be types, and let C be a family over x : A, y : B. Construct an

equivalence
   
swap-Σ : ∑(x:A) ∑(y:B) C ( x, y) ' ∑(y:B) ∑(x:A) C ( x, y) .
48 CHAPTER II. BASIC CONCEPTS OF TYPE THEORY

7.11 In this exercise we will show that the laws for abelian groups hold for addition
on the integers. Note: these are obvious facts, but the proof terms that show how
the group laws hold are nevertheless fairly involved. This exercise is perfect for a
formalization project.
(a) Show that addition satisfies the left and right unit laws, i.e., construct terms

left-unit-law-add-Z : ∏ (x:Z) 0 + x = x
right-unit-law-add-Z : ∏ (x:Z) x + 0 = x.

(b) Show that addition respects predecessors and successor on both sides, i.e.,
construct terms

left-predecessor-law-add-Z : ∏ (x,y:Z) predZ ( x ) + y = predZ ( x + y)

right-predecessor-law-add-Z : ∏ (x,y:Z) x + predZ (y) = predZ ( x + y)
left-successor-law-add-Z : ∏ (x,y:Z) succZ ( x ) + y = succZ ( x + y)
right-successor-law-add-Z : ∏ (x,y:Z) x + succZ (y) = succZ ( x + y).

Hint: to avoid an excessive number of cases, use induction on x but not on

y. You may need to use the homotopies succZ ◦ predZ ∼ id and predZ ◦ succZ
constructed in exercise Exercise 7.6.
(c) Use part (b) to show that addition on the integers is associative and commuta-
tive, i.e., construct terms

assoc-add-Z : ∏ (x,y,z:Z) ( x + y) + z = x + (y + z)
comm-add-Z : ∏ (x,y:Z) x + y = y + x.

Hint: Especially in the construction of the associator there is a risk of running

into an unwieldy amount of cases if you use Z-induction on all arguments.
Avoid induction on y and z.
(d) Show that addition satisfies the left and right inverse laws:

left-inverse-law-add-Z : ∏ (x:Z) (− x ) + x = 0
right-inverse-law-add-Z : ∏ (x:Z) x + (− x ) = 0.

Conclude that the functions y 7→ x + y and x 7→ x + y are equivalences for

any x : Z and y : Z, respectively.
7.12 In this exercise we will construct the functorial action of coproducts.
(a) Construct for any two maps f : A → A0 and g : B → B0 , a map

f + g : A + B → A0 + B0 .

(b) Show that if H : f ∼ f 0 and K : g ∼ g0 , then there is a homotopy

H + K : ( f + g ) ∼ ( f 0 + g 0 ).
8. CONTRACTIBLE TYPES AND CONTRACTIBLE MAPS 49

(c) Show that id A + idB ∼ id A+ B .

(d) Show that for any
f f0
A A0 A00
g g0
B B0 B00
there is a homotopy

( f 0 ◦ f ) + ( g 0 ◦ g ) ∼ ( f 0 + g 0 ) ◦ ( f ◦ g ).

(e) Show that if f and g are equivalences, then so is f + g. (The converse of this
statement also holds, see Exercise 9.5.)
7.13 Construct equivalences

Fin(m + n) ' Fin(m) + Fin(n)

Fin(mn) ' Fin(m) × Fin(n).

8 Contractible types and contractible maps

A contractible type is a type which has, up to identification, only one term. In other words,
a contractible type is a type that comes equipped with a point, and an identification of
this point with any point.
We may think of contractible types as singletons up to homotopy, and indeed we
show that the unit type is an example of a contractible type. Moreover, we show that
contractible types satisfy an induction principle that is very similar to the induction
principle of the unit type, provided that we formulate the computation rule using the
identity type rather than postulating a judgmental computation rule. Another example
of a contractible type is the total space of the family of identifications with a fixed starting
point.
We then introduce the notion of fiber of a map, which is the type theoretic analogue
of the pre-image of a map, and we say that a map in contractible if all its fibers are
contractible. Thus, a map is contractible if the pre-image at any point in the codomain
is a singleton. This condition is of course analogous to the set theoretic notion of
bijective map, which suggests that on the type theoretical side of things a map should be
contractible if and only if it is an equivalence.
The forward direction of this claim is straightforward, and we prove this direction
immediately in Theorem 8.2.5. The converse direction can be done directly, but it is
certainly more involved. Therefore we prepare the proof of the converse direction by first
characterizing the identity type of a fiber of a map. Then we show that any equivalence
e can be given the structure of a invertible map with an additional coherence relating the
homotopies
e ◦ e−1 ∼ id, and e−1 ◦ e ∼ id,
and finally we use these observations in Theorem 8.3.6 to conclude that the fibers of any
equivalence must be contractible.
50 CHAPTER II. BASIC CONCEPTS OF TYPE THEORY

8.1 Contractible types

Definition 8.1.1. We say that a type A is contractible if it comes equipped with a term
of type
is-contr( A) :≡ ∑(c:A) ∏ (x:A) c = x.
Given a term (c, C ) : is-contr( A), we call c : A the center of contraction of A, and we
call C : ∏ (x:A) c = x the contraction of A.

Remark 8.1.2. Suppose A is a contractible type with center of contraction c and contraction
C. Then the type of C is (judgmentally) equal to the type

constc ∼ id A .

In other words, the contraction C is a homotopy from the constant function to the identity
function.
Example 8.1.3. The unit type is easily seen to be contractible. For the center of contraction
we take ? : 1. Then we define a contraction ∏ (x:1) ? = x by the induction principle of 1.
Applying the induction principle, it suffices to construct a term of type ? = ?, for which
we just take refl? .

Definition 8.1.4. Suppose A comes equipped with a term a : A. Then we say that A
satisfies singleton induction if for every type family B over A, the map
 
ev-pt : ∏ (x:A) B( x ) → B( a)

defined by ev-pt( f ) :≡ f ( a) has a section. In other words, if A satisfies singleton

induction we have a function and a homotopy

sing-inda : B( a) → ∏ (x:A) B( x )
sing-compa : ev-pt ◦ sing-inda ∼ id

for any type family B over A.

Example 8.1.5. Note that the singleton induction principle is almost the same as the
induction principle for the unit type, the difference being that the "computation rule" in
the singleton induction for A is stated using an identification rather than as a judgmental
equality. The unit type 1 comes equipped with a function

ind1 : B(?) → ∏ (x:1) B( x )

for every type family B over 1, satisfying the judgmental equality ind1 (b, ?) ≡ b for every
b : B(?) by the computation rule. Thus we easily obtain the homotopy

λb. reflb : ev-pt ◦ ind1 ∼ id,

and we conclude that the unit type satisfies singleton induction.

Theorem 8.1.6. Let A be a type. The following are equivalent:

8. CONTRACTIBLE TYPES AND MAPS 51

(i) The type A is contractible.

(ii) The type A comes equipped with a term a : A, and satisfies singleton induction.

Proof. Suppose A is contractible with center of contraction c and contraction C. First we

observe that, without loss of generality, we may assume that C comes equipped with
an identification p : C (c) = reflc . To see this, note that we can always define a new
contraction C 0 by
C 0 ( x ) : ≡ C ( c ) −1  C ( x ),
which satisfies the requirement by the left inverse law, constructed in Definition 5.2.5.
To show that A satisfies singleton induction let B be a type family over A equipped
with b : B( a). To define sing-inda (b) : ∏ (x:A) B( x ), let x : A. We have an identification
C ( x ) : a = x, and b is in B( a). Therefore we can transport b along the path C ( x ) to obtain

sing-inda (b) :≡ tr B (C ( x ), b) : B( x ).

To see that sing-ind(c) = b note that we have

apλω. tr
B (ω,b)
( p) reflb
tr B (C (c), b) tr B (reflc , b) b.

This completes the proof that A satisfies singleton induction.

For the converse, suppose that a : A and that A satisfies singleton induction. Our
goal is to show that A is contractible. For the center of contraction we take the term a : A.
By singleton induction applied to B( x ) :≡ a = x we have the map

sing-inda : a = a → ∏ (x:A) a = x.

Therefore sing-ind A,a (refla ) is a contraction.

Theorem 8.1.7. For any a : A, the type

∑(x:A) a = x

is contractible.

Proof. We will prove the statement by showing that ∑(y:A) x = y satisfies singleton
induction, and then use Theorem 8.1.6 to conclude that ∑(x:A) a = x is contractible. We
will use the term ( a, refla ) : ∑(x:A) a = x as the center of contraction.
Now let P be a type family over ∑(x:A) a = x. Note that we have a commuting
triangle
ev-pair
∏ (t:∑(x:A) a= x) P(t) ∏ (x:A) ∏ ( p:a= x) P( x, p)

ev-pt ev-refl
P( a, refla )

where the maps ev-pair and ev-refl are defined as

f 7→ λx. λp. f ( x, p)
52 CHAPTER II. BASIC CONCEPTS OF TYPE THEORY

g 7→ g( a, refla ),

respectively. By the induction principle for Σ-types it follows that ev-pair has a section,
and by path induction it follows that ev-refl has a section. Therefore it follows from
Exercise 7.4 that the composite ev-pt has a section.

8.2 Contractible maps

Definition 8.2.1. Let f : A → B be a function, and let b : B. The fiber of f at b is defined
to be the type
fib f (b) :≡ ∑(a:A) f ( a) = b.

In other words, the fiber of f at b is the type of a : A that get mapped by f to b. One
may think of the fiber as a type theoretic version of the pre-image of a point.
It will be useful to have a characterization of the identity type of a fiber, so we will
make such a characterization immediately.

Definition 8.2.2. Let f : A → B be a map, and let ( x, p), ( x 0 , p0 ) : fib f (y) for some y : B.
Then we define

Eq-fib f (( x, p), ( x 0 , p0 )) :≡ ∑(α:x= x0 ) p = ap f (α)  p0

The relation Eq-fib f : fib f (y) → fib f (y) → U is a reflexive relation, since we have

λ( x, p). (reflx , refl p ) : ∏ ((x,p):fib f (y)) Eq-fib f (( x, p), ( x, p)).

Lemma 8.2.3. Consider a map f : A → B and let y : B. The canonical map

(( x, p) = ( x 0 , p0 )) → Eq-fib f (( x, p), ( x 0 , p0 ))

induced by the reflexivity of Eq-fib f is an equivalence for any ( x, p), ( x 0 , p0 ) : fib f (y).

Proof. The converse map

Eq-fib f (( x, p), ( x 0 , p0 )) → (( x, p) = ( x 0 , p0 ))

is easily defined by Σ-induction, and then path induction twice. The homotopies witness-
ing that this converse map is indeed a right inverse as well as a left inverse is similarly
constructed by induction.

Now we arrive at the notion of contractible map.

Definition 8.2.4. We say that a function f : A → B is contractible if there is a term of

type
is-contr( f ) :≡ ∏ (b:B) is-contr(fib f (b)).

Theorem 8.2.5. Any contractible map is an equivalence.

8. CONTRACTIBLE TYPES AND MAPS 53

Proof. Let f : A → B be a contractible map. Using the center of contraction of each

fib f (y), we obtain a term of type

λy. ( g(y), G (y)) : ∏ (y:B) fib f (y).

Thus, we get map g : B → A, and a homotopy G : ∏ (y:B) f ( g(y)) = y. In other words,

we get a section of f .
It remains to construct a retraction of f . Taking g as our retraction, we have to show
that ∏ (x:A) g( f ( x )) = x. Note that we get an identification p : f ( g( f ( x ))) = f ( x ) since
g is a section of f . It follows that ( g( f ( x )), p) : fib f ( f ( x )). Moreover, since fib f ( f ( x )) is
contractible we get an identification q : ( g( f ( x )), p) = ( x, refl f (x) ). The base path appr1 (q)
of this identification is an identification of type g( f ( x )) = x, as desired.

8.3 Equivalences are contractible maps

In Theorem 8.3.6 we will show the converse to Theorem 8.2.5, i.e., we will show that any
equivalence is a contractible map. We will do this in two steps.
First we introduce a new notion of coherently invertible map, for which we can easily
show that such maps have contractible fibers. Then we show that any equivalence is a
coherently invertible map.
Recall that an invertible map is a map f : A → B equipped with g : B → A and
homotopies
G : f ◦ g ∼ id and H : g ◦ f ∼ id.

Then we observe that both G · f and f · H are homotopies of the same type

f ◦ g ◦ f ∼ f.

A coherently invertible map is an invertible map for which there is a further homotopy
G · f ∼ f · H.

Definition 8.3.1. Consider a map f : A → B. We say that f is coherently invertible if it

comes equipped with

g:B→A
G : f ◦ g ∼ id
H : g ◦ f ∼ id
K : G · f ∼ f · H.

We will write is-coh-invertible( f ) for the type of quadruples ( g, G, H, K ).

Although we will encounter the notion of coherently invertible map on some further
occasions, the following lemma is our main motivation for considering it.

Lemma 8.3.2. Any coherently invertible map has contractible fibers.

54 CHAPTER II. BASIC CONCEPTS OF TYPE THEORY

Proof. Consider a map f : A → B equipped with

g:B→A
G : f ◦ g ∼ id
H : g ◦ f ∼ id
K : G · f ∼ f · H,
and let y : B. Our goal is to show that fib f (y) is contractible. For the center of contraction
we take ( g(y), G (y)). In order to construct a contraction, it suffices to construct a term of
type
∏ (x:A) ∏ ( p: f (x)=y) Eq-fib f (( g(y), G (y)), ( x, p)).
By path induction on p : f ( x ) = y it suffices to construct a term of type
∏ (x:A) Eq-fib f (( g( f ( x )), G ( f ( x ))), ( x, refl f (x) )).
By definition of Eq-fib f , we have to construct a term of type
∏ (x:A) ∑(α:g( f (x))=x) G ( f ( x )) = ap f (α)  refl f (x) .
Such a term is constructed as λx. ( H ( x ), K 0 ( x )), where the homotopy H : g ◦ f ∼ id is
given by assumption, and the homotopy

K 0 : ∏ (x:A) G ( f ( x )) = ap f ( H ( x ))  refl f (x)

is defined as
K 0 :≡ K  htpy-right-unit( f · H )−1 .
Our next goal is to show that for any map f : A → B equipped with
g : B → A, G : f ◦ g ∼ id, and H : g ◦ f ∼ id,
we can improve the homotopy G to a new homotopy G 0 : f ◦ g ∼ id for which there is a
further homotopy
f · H ∼ G0 · f .
Note that this situation is analogous to the situation in the proof of Theorem 8.1.6, where
we improved the contraction C so that it satisfied C (c) = refl. The extra coherence
f · H ∼ G 0 · f is then used in the proof that the fibers of an equivalence are contractible.
Definition 8.3.3. Let f , g : A → B be functions, and consider H : f ∼ g and p : x = y in
A. We define the identification
htpy-nat( H, p) :≡ ap f ( p)  H (y) = H ( x )  apg ( p)
witnessing that the square
H (x)
f (x) g( x )
ap f ( p) apg ( p)

f (y) g(y)
H (y)

commutes. This square is also called the naturality square of the homotopy H at p.
8. CONTRACTIBLE TYPES AND MAPS 55

Construction. By path induction on p it suffices to construct an identification

ap f (reflx )  H ( x ) = H ( x )  apg (reflx )

since ap f (reflx ) ≡ refl f (x) and apg (reflx ) ≡ reflg(x) , and since refl f (x)  H ( x ) ≡ H ( x ), we
see that the path right-unit( H ( x ))−1 is of the asserted type.

Definition 8.3.4. Consider f : A → A and H : f ∼ id A . We construct an identification

H ( f ( x )) = ap f ( H ( x )), for any x : A.

Construction. By the naturality of homotopies with respect to identifications the square

H ( f ( x ))
f f (x) f (x)
ap f ( H ( x )) H (x)

f (x) x
H (x)

commutes. This gives the desired identification H ( f ( x )) = ap f ( H ( x )).

Lemma 8.3.5. Let f : A → B be a map, and consider ( g, G, H ) : has-inverse( f ). Then there is

a homotopy G 0 : f ◦ g ∼ id equipped with a further homotopy

K : G 0 · f ∼ f · H.

Thus we obtain a map has-inverse( f ) → is-coh-invertible( f ).

Proof. For each y : B, we construct the identification G 0 (y) as the concatenation

G ( f g(y))−1 ap f ( H ( g(y))) G (y)

f g(y) f g f g(y) f g(y) y.

In order to construct a homotopy G 0 · f ∼ f · H, it suffices to show that the square

G ( f g f ( x ))
f g f g f (x) f g f (x)
ap f ( H ( g f ( x ))) ap f ( H ( x ))

f g f (x) f (x)
G ( f ( x ))

commutes for every x : A. Recall from Definition 8.3.4 that we have H ( g f ( x )) =

apg f ( H ( x )). Using this identification, we see that it suffices to show that the square

G ( f g f ( x ))
f g f g f (x) f g f (x)
ap f g f ( H ( x )) ap f ( H ( x ))

f g f (x) f (x)
G ( f ( x ))

commutes. Now we observe that this is just a naturality square the homotopy G f :
f g f ∼ f , which commutes by Definition 8.3.3.
56 CHAPTER II. BASIC CONCEPTS OF TYPE THEORY

Now we put the pieces together to conclude that any equivalence has contractible
fibers.
Theorem 8.3.6. Any equivalence is a contractible map.
Proof. We have seen in Lemma 8.3.2 that any coherently invertible map is a contractible
map. Moreover, any equivalence has the structure of an invertible map by Lemma 7.2.3,
and any invertible map is coherently invertible by Lemma 8.3.5.
Corollary 8.3.7. Let A be a type, and let a : A. Then the type
∑(x:A) x = a
is contractible.
Proof. By Remark 7.2.5, the identity function is an equivalence. Therefore, the fibers of
the identity function are contractible by Theorem 8.3.6. Note that ∑(x:A) x = a is exactly
the fiber of id A at a : A.

Exercises
8.1 Show that if A is contractible, then for any x, y : A the identity type x = y is also
contractible.
8.2 Suppose that A is a retract of B. Show that
is-contr( B) → is-contr( A).
8.3 (a) Show that for any type A, the map const? : A → 1 is an equivalence if and
only if A is contractible.
(b) Apply Exercise 7.4 to show that for any map f : A → B, if any two of the
three assertions
(i) A is contractible
(ii) B is contractible
(iii) f is an equivalence
hold, then so does the third.
8.4 Show that for any two types A and B, the following are equivalent:
(i) Both A and B are contractible.
(ii) The type A × B is contractible.
8.5 Let A be a contractible type with center of contraction a : A. Furthermore, let B
be a type family over A. Show that the map y 7→ ( a, y) : B( a) → ∑(x:A) B( x ) is an
equivalence.
8.6 Let B be a family of types over A, and consider the projection map
pr1 : ∑(x:A) B( x ) → A.

Show that for any a : A, the map

λ(( x, y), p). tr B ( p, y) : fibpr1 ( a) → B( a),
is an equivalence. Conclude that pr1 is an equivalence if and only if each B( a) is
contractible.
9. THE FUNDAMENTAL THEOREM OF IDENTITY TYPES 57

8.7 Construct for any map f : A → B an equivalence e : A ' ∑(y:B) fib f (y) and a
homotopy H : f ∼ pr1 ◦ e witnessing that the triangle
e
A ∑(y:B) fib f (y)

f pr1
B

commutes. The projection pr1 : (∑(y:B) fib f (y)) → B is sometimes also called
the fibrant replacement of f , because first projection maps are fibrations in the
homotopy interpretation of type theory.

9 The fundamental theorem of identity types

For many types it is useful to have a characterization of their identity types. For example,
we have used a characterization of the identity types of the fibers of a map in order to
conclude that any equivalence is a contractible map. The fundamental theorem of identity
types is our main tool to carry out such characterizations, and with the fundamental
theorem it becomes a routine task to characterize an identity type whenever that is of
interest.
Our first application of the fundamental theorem of identity types in the present
lecture is a simple proof that any equivalence is an embedding. Embeddings are maps
that induce equivalences on identity types, i.e., they are the homotopical analogue
of injective maps. In our second application we characterize the identity types of
coproducts.
Throughout the rest of this book we will encounter many more occasions to charac-
terize identity types. For example, we will show in Theorem 10.2.6 that the identity type
of the natural numbers is equivalent to its observational equality, and we will show in
Theorem 15.5.2 that the loop space of the circle is equivalent to Z.
In order to prove the fundamental theorem of identity types, we first prove the
basic fact that a family of maps is a family of equivalences if and only if it induces an
equivalence on total spaces.

9.1 Families of equivalences

Definition 9.1.1. Consider a family of maps

f : ∏ (x:A) B( x ) → C ( x ).

We define the map

tot ( f ) : ∑(x:A) B( x ) → ∑(x:A) C ( x )
by λ( x, y). ( x, f ( x, y)).

Lemma 9.1.2. For any family of maps f : ∏ (x:A) B( x ) → C ( x ) and any t : ∑(x:A) C ( x ), there
is an equivalence
fibtot ( f ) (t) ' fib f (pr1 (t)) (pr2 (t)).
58 CHAPTER II. BASIC CONCEPTS OF TYPE THEORY

Proof. For any p : fibtot ( f ) (t) we define ϕ(t, p) : fibpr1 (t) (pr2 (t)) by Σ-induction on p.
Therefore it suffices to define ϕ(t, (s, α)) : fibpr1 (t) (pr2 (t)) for any s : ∑(x:A) B( x ) and
α : tot ( f )(s) = t. Now we proceed by path induction on α, so it suffices to define
ϕ(tot ( f )(s), (s, refl )) : fib f (pr1 (tot ( f )(s))) (pr2 (tot ( f )(s))). Finally, we use Σ-induction on s
once more, so it suffices to define

ϕ(( x, f ( x, y)), (( x, y), refl )) : fib f (x) ( f ( x, y)).

Now we take as our definition

ϕ(( x, f ( x, y)), (( x, y), refl )) :≡ (y, refl ).

For the proof that this map is an equivalence we construct a map

ψ(t) : fib f (pr1 (t)) (pr2 (t)) → fibtot ( f ) (t)

equipped with homotopies G (t) : ϕ(t) ◦ ψ(t) ∼ id and H (t) : ψ(t) ◦ ϕ(t) ∼ id. In each
of these definitions we use Σ-induction and path induction all the way through, until
an obvious choice of definition becomes apparent. We define ψ(t), G (t), and H (t) as
follows:

ψ(( x, f ( x, y)), (y, refl )) :≡ (( x, y), refl )

G (( x, f ( x, y)), (y, refl )) :≡ refl
H (( x, f ( x, y)), (( x, y), refl )) :≡ refl.

Theorem 9.1.3. Let f : ∏ (x:A) B( x ) → C ( x ) be a family of maps. The following are equivalent:

(i) For each x : A, the map f ( x ) is an equivalence. In this case we say that f is a family of
equivalences.

(ii) The map tot ( f ) : ∑(x:A) B( x ) → ∑(x:A) C ( x ) is an equivalence.

Proof. By Theorems 8.2.5 and 8.3.6 it suffices to show that f ( x ) is a contractible map
for each x : A, if and only if tot ( f ) is a contractible map. Thus, we will show that
fib f (x) (c) is contractible if and only if fibtot ( f ) ( x, c) is contractible, for each x : A and
c : C ( x ). However, by Lemma 9.1.2 these types are equivalent, so the result follows by
Exercise 8.3.

Now consider the situation where we have a map f : A → B, and a family C over B.
Then we have the map

λ( x, z). ( f ( x ), z) : ∑(x:A) C ( f ( x )) → ∑(y:B) C (y).

We claim that this map is an equivalence when f is an equivalence. The technique to

prove this claim is the same as the technique we used in Theorem 9.1.3: first we note
that the fibers are equivalent to the fibers of f , and then we use the fact that a map is an
equivalence if and only if its fibers are contractible to finish the proof.
9. THE FUNDAMENTAL THEOREM 59

Lemma 9.1.4. Consider an equivalence e : A ' B, and let C be a type family over B. Then the
map
σ f (C ) :≡ λ( x, z). ( f ( x ), z) : ∑(x:A) C ( f ( x )) → ∑(y:B) C (y)
is an equivalence.

Proof. We claim that for each t : ∑(y:B) C (y) there is an equivalence

fibσ f (C) (t) ' fib f (pr1 (t)).

We prove this by constructing

ϕ(t) : fibσ f (C) (t) → fib f (pr1 (t))

ψ(t) : fib f (pr1 (t)) → fibσ f (C) (t)
G (t) : ϕ ◦ ψ ∼ id
H (t) : ψ ◦ ϕ ∼ id.

The construction of these functions and homotopies is by using Σ-induction and path
induction all the way through, just as in the proof of Lemma 9.1.2. We list the definitions

ϕ(( f ( x ), z), (( x, z), refl )) :≡ ( x, refl )

ψ(( f ( x ), z), ( x, refl )) :≡ (( x, z), refl )
G (( f ( x ), z), ( x, refl )) :≡ refl
H (( f ( x ), z), (( x, z), refl )) :≡ refl.

Now the claim follows, since we see that ϕ is a contractible map if and only if f is a
contractible map.

We now combine Theorem 9.1.3 and Lemma 9.1.4.

Definition 9.1.5. Consider a map f : A → B and a family of maps

g : ∏ (x:A) C ( x ) → D ( f ( x )),

where C is a type family over A, and D is a type family over B. In this situation we also
say that g is a family of maps over f . Then we define

tot f ( g) : ∑(x:A) C ( x ) → ∑(y:B) D (y)

by tot f ( g)( x, z) :≡ ( f ( x ), g( x, z)).

Theorem 9.1.6. Suppose that g is a family of maps over f , and suppose that f is an equivalence.
Then the following are equivalent:

(i) The family of maps g over f is a family of equivalences.

(ii) The map tot f ( g) is an equivalence.

60 CHAPTER II. BASIC CONCEPTS OF TYPE THEORY

Proof. Note that we have a commuting triangle

tot f ( g)
∑(x:A) C ( x ) ∑(y:B) D (y)

tot ( g) λ( x,z). ( f ( x ),z)

∑(x:A) D ( f ( x ))

By the assumption that f is an equivalence, it follows that the map ∑(x:A) D ( f ( x )) →

∑(y:B) D (y) is an equivalence. Therefore it follows that tot f ( g) is an equivalence if and
only if tot ( g) is an equivalence. Now the claim follows, since tot ( g) is an equivalence if
and only if g if a family of equivalences.

9.2 The fundamental theorem

Many types come equipped with a reflexive relation that possesses a similar structure as
the identity type. The observational equality on the natural numbers is such an example.
We have see that it is a reflexive, symmetric, and transitive relation, and moreover it is
contained in any other reflexive relation. Thus, it is natural to ask whether observational
equality on the natural numbers is equivalent to the identity type.
The fundamental theorem of identity types (Theorem 9.2.2) is a general theorem that
can be used to answer such questions. It describes a necessary and sufficient condition
on a type family B over a type A equipped with a point a : A, for there to be a family
of equivalences ∏ (x:A) ( a = x ) ' B( x ). In other words, it tells us when a family B is a
characterization of the identity type of A.
Before we state the fundamental theorem of identity types we introduce the notion
of identity systems. Those are families B over a A that satisfy an induction principle that
is similar to the path induction principle, where the ‘computation rule’ is stated with an
identification.

Definition 9.2.1. Let A be a type equipped with a term a : A. A (unary) identity system
on A at a consists of a type family B over A equipped with b : B( a), such that for any
family of types P( x, y) indexed by x : A and y : B( x ), the function
 
h 7→ h( a, b) : ∏ (x:A) ∏ (y:B(x)) P( x, y) → P( a, b)

has a section.

The most important implication in the fundamental theorem is that (ii) implies
(i). Occasionally we will also use the third equivalent statement. We note that the
fundamental theorem also appears as Theorem 5.8.4 in [2].

Theorem 9.2.2. Let A be a type with a : A, and let B be be a type family over A with b : B( a).
Then the following are logically equivalent for any family of maps

f : ∏ (x:A) ( a = x ) → B( x ).

(i) The family of maps f is a family of equivalences.

9. THE FUNDAMENTAL THEOREM 61

(ii) The total space

∑(x:A) B( x )
is contractible.

(iii) The family B is an identity system.

In particular the canonical family of maps

path-inda (b) : ∏ (x:A) ( a = x ) → B( x )

is a family of equivalences if and only if ∑(x:A) B( x ) is contractible.

Proof. First we show that (i) and (ii) are equivalent. By Theorem 9.1.3 it follows that the
family of maps f is a family of equivalences if and only if it induces an equivalence
   
∑(x:A) a = x ' ∑(x:A) B( x )

on total spaces. We have that ∑(x:A) a = x is contractible. Now it follows by Exercise 8.3,
applied in the case

tot ( f )
∑(x:A) a = x ∑(x:A) B( x )

'
1

that tot ( f ) is an equivalence if and only if ∑(x:A) B( x ) is contractible.

Now we show that (ii) and (iii) are equivalent. Note that we have the following
commuting triangle

ev-pair
∏ (t:∑(x:A) B(x)) P(t) ∏ (x:A) ∏ (y:B(x)) P( x, y)

ev-pt( a,b) λh. h( a,b)

P( a, b)

In this diagram the top map has a section. Therefore it follows by Exercise 7.4 that the
left map has a section if and only if the right map has a section. Notice that the left map
has a section for all P if and only if ∑(x:A) B( x ) satisfies singleton induction, which is by
Theorem 8.1.6 equivalent to ∑(x:A) B( x ) being contractible.

9.3 Embeddings
As an application of the fundamental theorem we show that equivalences are embed-
dings. The notion of embedding is the homotopical analogue of the set theoretic notion
of injective map.
62 CHAPTER II. BASIC CONCEPTS OF TYPE THEORY

Definition 9.3.1. An embedding is a map f : A → B satisfying the property that

ap f : ( x = y) → ( f ( x ) = f (y))

is an equivalence for every x, y : A. We write is-emb( f ) for the type of witnesses that f is
an embedding.

Another way of phrasing the following statement is that equivalent types have
equivalent identity types.

Theorem 9.3.2. Any equivalence is an embedding.

Proof. Let e : A ' B be an equivalence, and let x : A. Our goal is to show that

ape : ( x = y) → (e( x ) = e(y))

is an equivalence for every y : A. By Theorem 9.2.2 it suffices to show that

∑(y:A) e( x ) = e(y)

is contractible for every y : A. Now observe that there is an equivalence

∑(y:A) e( x ) = e(y) ' ∑(y:A) e(y) = e( x )

≡ fibe (e( x ))

by Theorem 9.1.3, since for each y : A the map

inv : (e( x ) = e(y)) → (e(y) = e( x ))

is an equivalence by Exercise 7.1. The fiber fibe (e( x )) is contractible by Theorem 8.3.6, so
it follows by Exercise 8.3 that the type ∑(y:A) e( x ) = e(y) is indeed contractible.

9.4 Disjointness of coproducts

To give a second application of the fundamental theorem of identity types, we character-
ize the identity types of coproducts. Our goal in this section is to prove the following
theorem.

Theorem 9.4.1. Let A and B be types. Then there are equivalences

(inl( x ) = inl( x 0 )) ' ( x = x 0 )

(inl( x ) = inr(y0 )) ' ∅
(inr(y) = inl( x 0 )) ' ∅
(inr(y) = inr(y0 )) ' (y = y0 )

for any x, x 0 : A and y, y0 : B.

In order to prove Theorem 9.4.1, we first define a binary relation Eq-coprod A,B on the
coproduct A + B.
9. THE FUNDAMENTAL THEOREM 63

Definition 9.4.2. Let A and B be types. We define

Eq-coprod A,B : ( A + B) → ( A + B) → U

by double induction on the coproduct, postulating

Eq-coprod A,B (inl( x ), inl( x 0 )) :≡ ( x = x 0 )

Eq-coprod A,B (inl( x ), inr(y0 )) :≡ ∅
Eq-coprod A,B (inr(y), inl( x 0 )) :≡ ∅
Eq-coprod A,B (inr(y), inr(y0 )) :≡ (y = y0 )

The relation Eq-coprod A,B is also called the observational equality of coproducts.

Lemma 9.4.3. The observational equality relation Eq-coprod A,B on A + B is reflexive, and
therefore there is a map

Eq-coprod-eq : ∏ (s,t:A+ B) (s = t) → Eq-coprod A,B (s, t)

Construction. The reflexivity term ρ is constructed by induction on t : A + B, using

ρ(inl( x )) :≡ reflinl(x) : Eq-coprod A,B (inl( x ))

ρ(inr(y)) :≡ reflinr(y) : Eq-coprod A,B (inr(y)).

To show that Eq-coprod-eq is a family of equivalences, we will use the fundamental

theorem, Theorem 9.2.2. Moreover, we will use the functoriality of coproducts (estab-
lished in Exercise 7.12), along with the following facts about Σ-types, coproducts, and
the empty type:
   
∑(t:A+ B) P(t) ' ∑(x:A) P(inl( x )) + ∑(y:B) P(inr(y))

∑(x:A) ∅ ' ∅
A + ∅ ' A.

All of these equivalences are straightforward to construct, so we leave them as an exercise

to the reader.

Lemma 9.4.4. For any s : A + B the total space

∑(t:A+ B) Eq-coprod A,B (s, t)

is contractible.

Proof. We will do the proof by induction on s. The two cases are similar, so we only
show that the total space

∑(t:A+ B) Eq-coprod A,B (inl( x ), t)

64 CHAPTER II. BASIC CONCEPTS OF TYPE THEORY

is contractible. Note that we have equivalences

∑(t:A+ B) Eq-coprod A,B (inl( x ), t)

   
0 0
' ∑(x0 :A) Eq-coprod A,B (inl( x ), inl( x )) + ∑(y0 :B) Eq-coprod A,B (inl( x ), inr(y ))
   
' ∑(x0 :A) x = x 0 + ∑(y0 :B) ∅
 
' ∑(x0 :A) x = x 0 + ∅

' ∑(x0 :A) x = x 0 .

The latter type is contractible by Theorem 8.1.7.
Proof of Theorem 9.4.1. The proof is now concluded with an application of Theorem 9.2.2,
using Lemma 9.4.4.

Exercises
9.1 (a) Show that the map ∅ → A is an embedding for every type A.
(b) Show that inl : A → A + B and inr : B → A + B are embeddings for any two
types A and B.
9.2 Consider an equivalence e : A ' B. Construct an equivalence
(e( x ) = y) ' ( x = e−1 (y))
for every x : A and y : B.
9.3 Show that
( f ∼ g) → (is-emb( f ) ↔ is-emb( g))
for any f , g : A → B.
9.4 Consider a commuting triangle
h
A B

f g
X
with H : f ∼ g ◦ h.
(a) Suppose that g is an embedding. Show that f is an embedding if and only if h
is an embedding.
(b) Suppose that h is an equivalence. Show that f is an embedding if and only if
g is an embedding.
9.5 Consider two maps f : A → A0 and g : B → B0 .
(a) Show that if the map
f + g : ( A + B) → ( A0 + B0 )
is an equivalence, then so are both f and g (this is the converse of Exer-
cise 7.12.e).
9. EXERCISES 65

(b) Show that f + g is an embedding if and only if both f and g are embeddings.
9.6 (a) Let f , g : ∏ (x:A) B( x ) → C ( x ) be two families of maps. Show that
   
∏ (x:A) f ( x ) ∼ g( x ) → tot ( f ) ∼ tot ( g) .

(b) Let f : ∏ (x:A) B( x ) → C ( x ) and let g : ∏ (x:A) C ( x ) → D ( x ). Show that

tot (λx. g( x ) ◦ f ( x )) ∼ tot ( g) ◦ tot ( f ).

(c) For any family B over A, show that

tot (λx. idB(x) ) ∼ id.

9.7 Let a : A, and let B be a type family over A.

(a) Use Exercises 8.2 and 9.6 to show that if each B( x ) is a retract of a = x, then
B( x ) is equivalent to a = x for every x : A.
(b) Conclude that for any family of maps

f : ∏ (x:A) ( a = x ) → B( x ),

if each f ( x ) has a section, then f is a family of equivalences.

9.8 Use Exercise 9.7 to show that for any map f : A → B, if

ap f : ( x = y) → ( f ( x ) = f (y))

has a section for each x, y : A, then f is an embedding.

9.9 We say that a map f : A → B is path-split if f has a section, and for each x, y : A
the map
ap f ( x, y) : ( x = y) → ( f ( x ) = f (y))

also has a section. We write path-split( f ) for the type

sec( f ) × ∏ (x,y:A) sec(ap f ( x, y)).

Show that for any map f : A → B the following are equivalent:

(i) The map f is an equivalence.
(ii) The map f is path-split.
9.10 Consider a triangle
h
A B

f g
X

with a homotopy H : f ∼ g ◦ h witnessing that the triangle commutes.

66 CHAPTER II. BASIC CONCEPTS OF TYPE THEORY

(a) Construct a family of maps

fib-triangle(h, H ) : ∏ (x:X ) fib f ( x ) → fibg ( x ),

for which the square

tot (fib-triangle(h,H ))
∑(x:X ) fib f ( x ) ∑(x:X ) fibg ( x )

A B
h

commutes, where the vertical maps are as constructed in Exercise 8.7.

(b) Show that h is an equivalence if and only if fib-triangle(h, H ) is a family of
equivalences.

10 The hierarchy of homotopical complexity

10.1 Propositions and subtypes
Definition 10.1.1. A type A is said to be a proposition if there is a term of type

is-prop( A) :≡ ∏ (x,y:A) is-contr( x = y).

Given a universe U , we define PropU to be the type of all small propositions, i.e.,

PropU :≡ ∑(X:U ) is-prop( A).

Example 10.1.2. Any contractible type is a proposition by Exercise 8.1. However, proposi-
tions do not need to be inhabited: the empty type is also a proposition, since

∏ (x,y:∅) is-contr( x = y)

follows from the induction principle of the empty type.

In the following lemma we prove that in order to show that a type A is a proposition,
it suffices to show that any two terms of A are equal. In other words, propositions are
types with proof irrelevance.

Theorem 10.1.3. Let A be a type. Then the following are equivalent:

(i) The type A is a proposition.

(ii) Any two terms of type A can be identified, i.e., there is a dependent function

is-prop0 ( A) :≡ ∏ (x,y:A) x = y.

(iii) The type A is contractible as soon as it is inhabited, i.e., there is a function

A → is-contr( A).
10. HOMOTOPICAL COMPLEXITY 67

(iv) The map const? : A → 1 is an embedding.

Proof. To show that (i) implies (ii), let A be a proposition. Then its identity types are
contractible, so the center of contraction of x = y is identification x = y, for each x, y : A.
To show that (ii) implies (iii), suppose that A comes equipped with p : ∏ (x,y:A) x = y.
Then for any x : A the dependent function p( x ) : ∏ (y:A) x = y is a contraction of A. Thus
we obtain the function
λx. ( x, p( x )) : A → is-contr( A).
To show that (iii) implies (iv), suppose that A → is-contr( A) and let x, y : A. We have
to show that
apconst? : ( x = y) → (? = ?)
is an equivalence. Since we have x : A it follows that A is contractible. Since the unit
type is contractible it follows that const? is an equivalence. Therefore we conclude by
Theorem 9.3.2 that it is an embedding.
To show that (iv) implies (i), note that if A → 1 is an embedding, then the identity
types of A are equivalent to contractible types and therefore they must be contractible.

In the following lemma we show that propositions are closed under equivalences.
Lemma 10.1.4. Let A and B be types, and let e : A ' B. Then we have
is-prop( A) ↔ is-prop( B).
Proof. We will show that is-prop( B) implies is-prop( A). This suffices, because the con-
verse follows from the fact that e−1 : B → A is also an equivalence.
Since e is assumed to be an equivalence, it follows by Theorem 9.3.2 that
ape : ( x = y) → (e( x ) = e(y))
is an equivalence for any x, y : A. If B is a proposition, then in particular the type
e( x ) = e(y) is contractible for any x, y : A, so the claim follows from Theorem 8.3.6.
In set theory, a set y is said to be a subset of a set x, if any element of y is an element
of x, i.e., if the condition
∀z (z ∈ y) → (z ∈ x )
holds. We have already noted that type theory is different from set theory in that terms in
type theory come equipped with a unique type. Moreover, in set theory the proposition
x ∈ y is well-formed for any two sets x and y, whereas in type theory the judgment a : A
is only well-formed if it is derived using the postulated inference rules. Because of these
differences we must find a different way to talk about subtypes.
Note that in set theory there is a correspondence between the subsets of a set x,
and the predicates on x. A predicate on x is just a proposition P(z) that varies over the
elements z ∈ x. Indeed, if y is a subset of x, then the corresponding predicate is the
proposition z ∈ y. Conversely, if P is a predicate on x, then we obtain the subset
{z ∈ x | P(z)}
of x. Now we have the right idea of subtypes in type theory: they are families of
propositions.
68 CHAPTER II. BASIC CONCEPTS OF TYPE THEORY

Definition 10.1.5. A type family B over A is said to be a subtype of A if for each x : A

the type B( x ) is a proposition. When B is a subtype of A, we also say that B( x ) is a
property of x : A.

family B over A is a subtype of A if and

We will show in Corollary 10.3.8 that a type
only if the projection map pr1 : ∑(x:A) B( x ) → A is an embedding.

10.2 Sets
Definition 10.2.1. A type A is said to be a set if it comes equipped with a term of type

is-set( A) :≡ ∏ (x,y:A) is-prop( x = y).

Lemma 10.2.2. A type A is a set if and only if it satisfies axiom K, i.e., if and only if it comes
equipped with a term of type

axiom-K( A) :≡ ∏ (x:A) ∏ ( p:x= x) reflx = p.

Proof. If A is a set, then x = x is a proposition, so any two of its elements are equal. This
implies axiom K.
For the converse, if A satisfies axiom K, then for any p, q : x = y we have p  q−1 = reflx ,
and hence p = q. This shows that x = y is a proposition, and hence that A is a set.

Theorem 10.2.3. Let A be a type, and let R : A → A → U be a binary relation on A satisfying

(i) Each R( x, y) is a proposition,

(ii) R is reflexive, as witnessed by ρ : ∏ (x:A) R( x, x ),

(iii) There is a map

R( x, y) → ( x = y)
for each x, y : A.

Then any family of maps

∏ (x,y:A) ( x = y) → R( x, y)
is a family of equivalences. Consequently, the type A is a set.

Proof. Let f : ∏ (x,y:A) R( x, y) → ( x = y). Since R is assumed to be reflexive, we also have

a family of maps
path-indx (ρ( x )) : ∏ (y:A) ( x = y) → R( x, y).
Since each R( x, y) is assumed to be a proposition, it therefore follows that each R( x, y)
is a retract of x = y. Therefore it follows that ∑(y:A) R( x, y) is a retract of ∑(y:A) x = y,
which is contractible. We conclude that ∑(y:A) R( x, y) is contractible, and therefore that
any family of maps
∏ (y:A) ( x = y) → R( x, y)
is a family of equivalences.
Now it also follows that A is a set, since its identity types are equivalent to proposi-
tions, and therefore they are propositions by Lemma 10.1.4.
10. HOMOTOPICAL COMPLEXITY 69

Definition 10.2.4. A map f : A → B is said to be injective if for any x, y : A there is a

map
( f ( x ) = f (y)) → ( x = y).

Corollary 10.2.5. Any injective map into a set is an embedding.

Proof. Let f : A → B be an injective map between sets. Now consider the relation

R( x, y) :≡ ( f ( x ) = f (y)).

Note that R is reflexive, and that R( x, y) is a proposition for each x, y : A. Moreover, by

the assumption that f is injective, we have

R( x, y) → ( x = y)

for any x, y : A. Therefore we are in the situation of Theorem 10.2.3, so it follows that the
map ap f : ( x = y) → ( f ( x ) = f (y)) is an equivalence.

Theorem 10.2.6. The type of natural numbers is a set.

Proof. We will apply Theorem 10.2.3. Note that the observational equality EqN : N →
(N → U ) on N (Definition 6.4.2) is a reflexive relation by Exercise 6.1, and moreover
that EqN (n, m) is a proposition for every n, m : N (proof by double induction). Therefore
it suffices to show that
∏ (m,n:N) EqN (m, n) → (m = n).
This follows from the fact that observational equality is the least reflexive relation, which
was shown in Exercise 6.2.

10.3 General truncation levels

Definition 10.3.1. We define is-trunc : Z≥−2 → U → U by induction on k : Z≥−2 , taking

is-trunc−2 ( A) :≡ is-contr( A)
is-trunck+1 ( A) :≡ ∏ (x,y:A) is-trunck ( x = y).

For any type A, we say that A is k-truncated, or a k-type, if there is a term of type
is-trunck ( A). We say that a map f : A → B is k-truncated if its fibers are k-truncated.

Theorem 10.3.2. If A is a k-type, then A is also a (k + 1)-type.

Proof. We have seen in Example 10.1.2 that contractible types are propositions. This
proves the base case. For the inductive step, note that if any k-type is also a (k + 1)-type,
then any (k + 1)-type is a (k + 2)-type, since its identity types are k-types and therefore
(k + 1)-types.

Theorem 10.3.3. If e : A ' B is an equivalence, and B is a k-type, then so is A.

70 CHAPTER II. BASIC CONCEPTS OF TYPE THEORY

Proof. We have seen in Exercise 8.3 that if B is contractible and e : A ' B is an equiva-
lence, then A is also contractible. This proves the base case.
For the inductive step, assume that the k-types are stable under equivalences, and
consider e : A ' B where B is a (k + 1)-type. In Theorem 9.3.2 we have seen that

ape : ( x = y) → (e( x ) = e(y))

is an equivalence for any x, y. Note that e( x ) = e(y) is a k-type, so by the induction

hypothesis it follows that x = y is a k-type. This proves that A is a (k + 1)-type.

Corollary 10.3.4. If f : A → B is an embedding, and B is a (k + 1)-type, then so is A.

Proof. By the assumption that f is an embedding, the action on paths

ap f : ( x = y) → ( f ( x ) = f (y))

is an equivalence for every x, y : A. Since B is assumed to be a (k + 1)-type, it follows

that f ( x ) = f (y) is a k-type for every x, y : A. Therefore we conclude by Theorem 10.3.3
that x = y is a k-type for every x, y : A. In other words, A is a (k + 1)-type.

Theorem 10.3.5. Let B be a type family over A. Then the following are equivalent:

(i) For each x : A the type B( x ) is k-truncated. In this case we say that the family B is
k-truncated.

(ii) The projection map  

pr1 : ∑(x:A) B( x ) → A

is k-truncated.

Proof. By Exercise 8.6 we obtain equivalences

fibpr1 ( x ) ' B( x )

for every x : A. Therefore the claim follows from Theorem 10.3.3.

Theorem 10.3.6. Let f : A → B be a map. The following are equivalent:

(i) The map f is (k + 1)-truncated.

(ii) For each x, y : A, the map

ap f : ( x = y) → ( f ( x ) = f (y))

is k-truncated.

Proof. First we show that for any s, t : fib f (b) there is an equivalence

(s = t) ' fibap f (pr2 (s)  pr2 (t)−1 )

We do this by Σ-induction on s and t, and then we calculate

(( x, p) = (y, q)) ' Eq-fib f (( x, p), (y, q))

10. EXERCISES 71

≡ ∑(α:x=y) p = ap f (α)  q
' ∑(α:x=y) ap f (α)  q = p
' ∑(α:x=y) ap f (α) = p  q−1
≡ fibap f ( p  q−1 ).

By these equivalences, it follows that if ap f is k-truncated, then for each s, t : fib f (b)
the identity type s = t is equivalent to a k-truncated type, and therefore we obtain by
Theorem 10.3.3 that f is (k + 1)-truncated.
For the converse, note that we have equivalences

fibap f ( p) ' (( x, p) = (y, refl f (y) )).

It follows that if f is (k + 1)-truncated, then the identity type ( x, p) = (y, refl f (y) ) in
fib f ( f (y)) is k-truncated for any p : f ( x ) = f (y). We conclude by Theorem 10.3.3 that
the fiber fibap f ( p) is k-truncated.

Corollary 10.3.7. A map is an embedding if and only if its fibers are propositions.

Corollary 10.3.8. A type family B over A is a subtype if and only if the projection map
 
pr1 : ∑(x:A) B( x ) → A

is an embedding.

Theorem 10.3.9. Let f : ∏ (x:A) B( x ) → C ( x ) be a family of maps. Then the following are
equivalent:

(i) For each x : A the map f ( x ) is k-truncated.

(ii) The induced map    

tot ( f ) : ∑(x:A) B( x ) → ∑(x:A) C ( x )

is k-truncated.

Proof. This follows directly from Lemma 9.1.2 and Theorem 10.3.3.

Exercises
10.1 (a) Show that succN : N → N is an embedding.
(b) Show that n 7→ m + n is an embedding, for each m : N. Moreover, conclude
that there is an equivalence

fibaddN (m) (n) ' (m ≤ n).

(c) Show that n 7→ mn is an embedding, for each m > 0 in N. Conclude that the
divisibility relation
d|n
is a proposition for each d, n : N such that d > 0.
72 CHAPTER II. BASIC CONCEPTS OF TYPE THEORY

10.2 Let A be a type, and let the diagonal of A be the map δA : A → A × A given by
λx. ( x, x ).
(a) Show that
is-equiv(δA ) ↔ is-prop( A).
(b) Construct an equivalence fibδA (( x, y)) ' ( x = y) for any x, y : A.
(c) Show that A is (k + 1)-truncated if and only if δA : A → A × A is k-truncated.
10.3 (a) Let B be a type family over A. Show that if A is a k-type, and B( x ) is a k-type
for each x : A, then so is ∑(x:A) B( x ). Conclude that for any two k-types A and
B, the type A × B is also a k-type. Hint: for the base case, use Exercises 8.3
and 8.5.
(b) Show that for any k-type A, the identity types of A are also k-types.
(c) Show that any maps f : A → B between k-types A and B is a k-truncated
map.
(d) Use Exercise 8.6 to show that for any type family B : A → U , if A and
∑(x:A) B( x ) are k-types, then so is B( x ) for each x : A.
10.4 Show that 2 is a set by applying Theorem 10.2.3 with the observational equality on
2 defined in Exercise 6.5.
10.5 Show that for any two (k + 2)-types A and B, the disjoint sum A + B is again a
(k + 2)-type. Conclude that Z is a set.
10.6 Use Exercises 8.2 and 7.8 to show that if A is a retract of a k-type B, then A is also a
k-type.
10.7 Show that a type A is a (k + 1)-type if and only if the map constx : 1 → A is
k-truncated for every x : A.
10.8 Consider a commuting triangle

h
A B

f g
X

with H : f ∼ g ◦ h, and suppose that g is k-truncated. Show that f is k-truncated if

and only if h is k-truncated.
Chapter III

Univalent mathematics

11 Function extensionality
11.1 Equivalent forms of function extensionality
Definition 11.1.1. The axiom of function extensionality asserts that for any type family
B over A, and any two dependent functions f , g : ∏ (x:A) B( x ), the canonical map

htpy-eq : ( f = g) → ( f ∼ g)

that sends refl f to htpy-refl f is an equivalence. We will write eq-htpy for its inverse, if it is
assumed to exist.

In other words, the axiom of function extensionality asserts that for any two depen-
dent functions f , g : ∏ (x:A) B( x ), the type of identifications f = g is equivalent to the
type of homotopies f ∼ g from f to g. By the fundamental theorem of identity types
(Theorem 9.2.2) there are three equivalent ways of asserting function extensionality. In
the following theorem we state one further equivalent condition.

Theorem 11.1.2. The following are equivalent:

(i) The axiom of function extensionality.

(ii) For any type family B over A and any dependent function f : ∏ (x:A) B( x ), the total space

∑( g:∏ (x:A) B(x)) f ∼ g

is contractible.

(iii) The principle of homotopy induction: for any type family B over A, any dependent
function f : ∏ (x:A) B( x ), and any family of types P( g, H ) indexed by g : ∏ (x:A) B( x )
and H : f ∼ g, the evaluation function
 
∏ ( g:∏ (x:A) B(x)) ∏ ( H: f ∼ g) P( g, H ) → P( f , htpy-refl f )

given by s 7→ s( f , htpy-refl f ) has a section.

73
74 CHAPTER III. UNIVALENT MATHEMATICS

(iv) The weak function extensionality principle holds: For every type family B over A one
has    
∏ (x:A) is-contr( B( x )) → is-contr ∏ (x:A) B( x ) .

Proof. The fact that function extensionality is equivalent to (ii) and (iii) follows directly
from Theorem 9.2.2.
To show that function extensionality implies weak function extensionality, sup-
pose that each B( a) is contractible with center of contraction c( a) and contraction
Ca : ∏ (y:B(a)) c( a) = y. Then we take c :≡ λa. c( a) to be the center of contraction of
∏ (x:A) B( x ). To construct the contraction we have to define a term of type

∏ ( f :∏ (x:A) B(x)) c = f .

Let f : ∏ (x:A) B( x ). By function extensionality we have a map (c ∼ f ) → (c = f ), so it

suffices to construct a term of type c ∼ f . Here we take λa. Ca ( f ( a)). This completes the
proof that function extensionality implies weak function extensionality.
In the remaining part of the proof, we will show that weak function extensionality
implies that the type
∑( g:∏ (x:A) B(x)) f ∼ g
is contractible for any f : ∏ (x:A) B( x ). In order to do this, we first note that we have a
section-retraction pair
     
i r
∑( g:∏ (x:A) B(x)) f ∼g ∏ (x:A) ∑(b:B(x)) f (x) = b ∑( g:∏ (x:A) B(x)) f ∼g .

Here we have the functions

i :≡ λ( g, H ). λx. ( g( x ), H ( x ))
r :≡ λp. (λx. pr1 ( p( x )), λx. pr2 ( p( x ))).

Their composite is homotopic to the identity function by the computation rule for Σ-types
and the η-rule for Π-types:

r (i ( g, H )) ≡ r (λx. ( g( x ), H ( x )))
≡ (λx. g( x ), λx. H ( x ))
≡ ( g, H ).

Now we observe that the type ∏ (x:A) ∑(b:B(x)) f ( x ) = b is a product of contractible types,
so it is contractible by our assumption of the weak function extensionality principle. The
claim therefore follows, since retracts of contractible types are contractible by Exercise 8.2.

For the remainder of this chapter we will assume that the function extensionality ax-
iom holds. In Theorem 12.2.2 we will derive function extensionality from the univalence
axiom.
As a first application of the function extensionality axiom we generalize the weak
function extensionality axiom to k-types.
11. FUNCTION EXTENSIONALITY 75

Theorem 11.1.3. Assume function extensionality. Then for any type family B over A one has
   
∏ (x:A) is-trunck ( B( x )) → is-trunck ∏ (x:A) B( x ) .

Proof. The theorem is proven by induction on k ≥ −2. The base case is just the weak func-
tion extensionality principle, which was shown to follow from function extensionality in
Theorem 11.1.2.
For the inductive hypothesis, assume that the k-types are closed under dependent
function types. Assume that B is a family of (k + 1)-types. By function extensionality,
the type f = g is equivalent to f ∼ g for any two dependent functions f , g : ∏ (x:A) B( x ).
Now observe that f ∼ g is a dependent product of k-types, and therefore it is an k-type
by our inductive hypotheses. Therefore, it follows by Theorem 10.3.3 that f = g is an
k-type, and hence that ∏ (x:A) B( x ) is an (k + 1)-type.

Corollary 11.1.4. Suppose B is a k-type. Then A → B is also a k-type, for any type A.

11.2 The type theoretic principle of choice

The type theoretic principle of choice asserts that Π distributes over Σ. More precisely, it
asserts that the canonical map
   
choice : ∏ (x:A) ∑(y:B(x)) C ( x, y) → ∑( f :∏ (x:A) B(x)) ∏ (x:A) C ( x, f ( x ))

given by λh. (pr1 (h( x )), pr2 (h( x ))), is an equivalence. In order to see this as a principle of
choice, one can view the left hand side as the type of functions h that pick for every x : A
a term y : B( x ) equipped with a term of type C ( x, y). The function choice then constructs
a dependent function f : ∏ (x:A) B( x ) equipped with a term of type ∏ (x:A) C ( x, f ( x )). In
this section we show that the map choice is an equivalence, and we use this to characterize
the identity of any dependent function type ∏ (x:A) B( x ) in terms of any characterization
of the identity types of the individual types B( x ).

Theorem 11.2.1. Consider a family of types C ( x, y) indexed by x : A and y : B( x ). Then the

map    
choice : ∏ (x:A) ∑(y:B(x)) C ( x, y) → ∑( f :∏ (x:A) B(x)) ∏ (x:A) C ( x, f ( x ))

given by λh. (pr1 (h( x )), pr2 (h( x ))) is an equivalence.

Proof. We define the map

   
choice−1 : ∑( f :∏ (x:A) B(x)) ∏ (x:A) C ( x, f ( x )) → ∏ (x:A) ∑(y:B(x)) C ( x, y)

by λ( f , g). λx. ( f ( x ), g( x )). Then we have to construct homotopies

choice ◦ choice−1 ∼ id, and choice−1 ◦ choice ∼ id.

For the first homotopy it suffices to construct an identification

choice(choice−1 ( f , g)) = ( f , g)
76 CHAPTER III. UNIVALENT MATHEMATICS

for any f : ∏ (x:A) B( x ) and any g : ∏ (x:A) C ( x, f ( x )). We compute the left-hand side as
follows:

choice(choice−1 ( f , g)) ≡ choice(λx. ( f ( x ), g( x )))

≡ (λx. f ( x ), λx. g( x )).

By the η-rule it follows that f ≡ λx. f ( x ) and g ≡ λx. g( x ). Therefore we have the
identification
refl( f ,g) : choice(choice−1 ( f , g)) = ( f , g).
This completes the construction of the first homotopy.
For the second homotopy we have to construct an identification

choice−1 (choice(h)) = h

for any h : ∏ (x:A) ∑(y:B(x)) C ( x, y). We compute the left-hand side as follows:

choice−1 (choice(h)) ≡ choice−1 (λx. pr1 (h( x )), (λx. pr2 (h( x ))))
≡ λx. (pr1 (h( x )), pr2 (h( x )))

However, it is not the case that (pr1 (h( x )), pr2 (h( x ))) ≡ h( x ) for any h : ∏ (x:A) ∑(y:B(x)) C ( x, y).
Nevertheless, we have the identification

eq-pair(refl, refl ) : (pr1 (h( x )), pr2 (h( x ))) = h( x ).

Therefore we obtain the required homotopy by function extensionality:

λh. eq-htpy(λx. eq-pair(reflpr1 (h(x)) , reflpr2 (h(x)) )) : choice−1 ◦ choice ∼ id.

Corollary 11.2.2. For type A and any type family C over B, the map
   
∑( f :A→ B) ∏ (x:A) C ( f ( x )) → A → ∑(y:B) C ( x )

given by λ( f , g). λx. ( f ( x ), g( x )) is an equivalence.

Remark 11.2.3. The type theoretic choice principle can be used to derive the binomial
theorem. We give an informal argument of how this goes. Recall that the binomial
theorem asserts that
k  
k l k−l
(n + m) = ∑
k
nm
l =0
l
for any three natural numbers k, m, n.
Consider the types A :≡ Fin(k ), B :≡ Fin(n) and C :≡ Fin(m). Then we can define
the type family P : 2 → U given by

P (12 ) : ≡ B
P(02 ) :≡ C.
11. FUNCTION EXTENSIONALITY 77

Now, the type theoretic principle of choice gives us an equivalence

   
∏ (x:A) ∑(t:2) P(t) ' ∑( f :A→2) ∏ (x:A) P( f ( x )) .

Now we note that the type ( f ( x ) = 1) + ( f ( x ) = 0) is contractible for any f : A → 2

and x : A. Therefore we have equivalences

∑( f :A→2) ∏ (x:A) P( f ( x ) ' ∑( f :A→2) ∏ (x:A) ∏ (t:( f (x)=1)+( f (x)=0)) P( f ( x ))

' ∑( f :A→2) (fib f (1) → B) × (fib f (0) → C )

Now we note that, because there are (kl) ways to choose a subset of l elements of A, there
are
k  
k
∑ l nl mk−l
l =0

elements in the above type.

11.3 Universal properties

The function extensionality principle allows us to prove universal properties. Universal
properties are characterizations of all maps out of or into a given type, so they are very
important. Among other applications, universal properties characterize a type up to
equivalence. In the following theorem we prove the universal property of dependent
pair types.

Theorem 11.3.1. Let B be a type family over A, and let X be a type. Then the map
    
ev-pair : ∑(x:A) B( x ) → X → ∏ (x:A) ( B( x ) → X )

given by f 7→ λa. λb. f ( a, b) is an equivalence.

Proof. The map in the converse direction is simply

    
indΣ : ∏ (x:A) ( B( x ) → X ) → ∑(x:A) B( x ) → X .

By the computation rules for Σ-types we have

λ f . refl f : ev-pair ◦ indΣ ∼ id

To show that indΣ ◦ ev-pair ∼ id we will also apply function extensionality. Thus, it
suffices to show that indΣ (λx. λy. f (( x, y))) = f . We apply function extensionality again,
so it suffices to show that

∏ (t:∑(x:A) B(x)) indΣ λx. λy. f (( x, y)) (t) = f (t).

We obtain this homotopy by another application of Σ-induction.

78 CHAPTER III. UNIVALENT MATHEMATICS

Corollary 11.3.2. Let A, B, and X be types. Then the map

ev-pair : ( A × B → X ) → ( A → ( B → X ))

given by f 7→ λa. λb. f (( a, b)) is an equivalence.

The universal property of identity types is sometimes called the type theoretical Yoneda
lemma: families of maps out of the identity type are uniquely determined by their action
on the reflexivity identification.

Theorem 11.3.3. Let B be a type family over A, and let a : A. Then the map
 
ev-refl : ∏ (x:A) ( a = x ) → B( x ) → B( a)

given by λ f . f ( a, refla ) is an equivalence.

Proof. The inverse ϕ is defined by path induction, taking b : B( a) to the function f

satisfying f ( a, refla ) ≡ b. It is immediate that ev-refl ◦ ϕ ∼ id.
To see that ϕ ◦ ev-refl ∼ id, let f : ∏ (x:A) ( a = x ) → B( x ). To show that ϕ( f ( a, refla )) =
f we use function extensionality (twice), so it suffices to show that

∏ (x:A) ∏ ( p:a= x) ϕ( f ( a, refla ), x, p) = f ( x, p).

This follows by path induction on p, since ϕ( f ( a, refla ), a, refla ) ≡ f ( a, refla ).

11.4 Composing with equivalences

We show in this section that a map f : A → B is an equivalence if and only if for any
type X the precomposition map

– ◦ f : (B → X) → ( A → X)

is an equivalence. Moreover, we will show in Theorem 11.4.1 that the ‘dependent version’
of this statement also holds: a map f : A → B is an equivalence if and only if for any
type family P over B, the precomposition map
   
– ◦ f : ∏ (y:B) P(y) → ∏ (x:A) P( f ( x ))

is an equivalence.

Theorem 11.4.1. For any map f : A → B, the following are equivalent:

(i) f is an equivalence.

(ii) For any type family P over B the map

   
∏ (y:B) P(y) → ∏ (x:A) P( f ( x ))

given by h 7→ h ◦ f is an equivalence.
11. FUNCTION EXTENSIONALITY 79

(iii) For any type X the map

(B → X) → ( A → X)
given by g 7→ g ◦ f is an equivalence.

Proof. To show that (i) implies (ii), we first recall from Lemma 8.3.5 that any equivalence
is also coherently invertible. Therefore f comes equipped with

g:B→A
G : f ◦ g ∼ idB
H : g ◦ f ∼ id A
K : G · f ∼ f · H.

Then we define the inverse of – ◦ f to be the map

   
ϕ : ∏ (x:A) P( f ( x )) → ∏ (y:B) P(y)

given by h 7→ λy. tr P ( G (y), h( g(y))).

To see that ϕ is a section of – ◦ f , let h : ∏ (x:A) P( f ( x )). By function extensionality it
suffices to construct a homotopy ϕ(h) ◦ f ∼ h. In other words, we have to show that

tr P ( G ( f ( x )), h( g( f ( x ))) = h( x )

for any x : A. Now we use the additional homotopy K from our assumption that f is
coherently invertible. Since we have K ( x ) : G ( f ( x )) = ap f ( H ( x )) it suffices to show that

tr P (ap f ( H ( x )), hg f ( x )) = h( x ).

A simple path-induction argument yields that

tr P (ap f ( p)) ∼ tr P◦ f ( p)

for any path p : x = y in A, so it suffices to construct an identification

tr P◦ f ( H ( x ), hg f ( x )) = h( x ).

We have such an identification by apdh ( H ( x )).

To see that ϕ is a retraction of – ◦ f , let h : ∏ (y:B) P(y). By function extensionality it
suffices to construct a homotopy ϕ(h ◦ f ) ∼ h. In other words, we have to show that

tr P ( G (y), h f g(y)) = h(y)

for any y : B. We have such an identification by apdh ( G (y)). This completes the proof
that (i) implies (ii).
Note that (iii) is an immediate consequence of (ii), since we can just choose P to be
the constant family X.
It remains to show that (iii) implies (i). Suppose that

– ◦ f : (B → X) → ( A → X)
80 CHAPTER III. UNIVALENT MATHEMATICS

is an equivalence for every type X. Then its fibers are contractible by Theorem 8.3.6. In
particular, choosing X ≡ A we see that the fiber

fib – ◦ f (id A ) ≡ ∑(h:B→ A) h ◦ f = id A

is contractible. Thus we obtain a function h : B → A and a homotopy H : h ◦ f ∼ id A

showing that h is a retraction of f . We will show that h is also a section of f . To see this,
we use that the fiber
fib – ◦ f ( f ) ≡ ∑(i:B→ B) i ◦ f = f
is contractible (choosing X ≡ B). Of course we have (idB , refl f ) in this fiber. However we
claim that there also is an identification p : ( f ◦ h) ◦ f = f , showing that ( f ◦ h, p) is in
this fiber, because

( f ◦ h) ◦ f ≡ f ◦ (h ◦ f )
= f ◦ id A
≡ f
Now we conclude by the contractibility of the fiber that (idB , refl f ) = ( f ◦ h, p). In
particular we obtain that idB = f ◦ h, showing that h is a section of f .

Exercises
11.1 Show that the functions

htpy-inv : ( f ∼ g) → ( g ∼ f )
htpy-concat( H ) : ( g ∼ h) → ( f ∼ h)
htpy-concat0 (K ) : ( f ∼ g) → ( f ∼ h)

are equivalences for every f , g, h : ∏ (x:A) B( x ). Here, htpy-concat0 (K ) is the function

defined by H 7→ H  K.
11.2 (a) Show that for any type A the type is-contr( A) is a proposition.
(b) Show that for any type A and any k ≥ −2, the type is-trunck ( A) is a proposi-
tion.
11.3 Let f : X → Y be a map. Show that the following are equivalent:
(i) f is an equivalence.
(ii) The map f ◦ – : X A → Y A is an equivalence for every type A.
11.4 Let f : A → B be a function.
(a) Show that if f is an equivalence, then the type ∑( g:B→ A) f ◦ g ∼ id of sections
of f is contractible.
(b) Show that if f is an equivalence, then the type ∑(h:B→ A) h ◦ f ∼ id of retrac-
tions of f is contractible.
(c) Show that is-equiv( f ) is a proposition.
(d) Use Exercises 11.2 and 11.5 to show that is-equiv( f ) ' is-contr( f ).
Conclude that A ' B is a subtype of A → B, and in particular that the map
pr1 : ( A ' B) → ( A → B) is an embedding.
11. EXERCISES 81

11.5 (a) Let P and Q be propositions. Show that

( P ↔ Q ) ' ( P ' Q ).
(b) Show that P is a proposition if and only if P → P is contractible.
11.6 Show that path-split( f ) and is-coh-invertible( f ) are propositions for any map f :
A → B. Conclude that we have equivalences

is-equiv( f ) ' path-split( f ) ' is-coh-invertible( f ).

11.7 Construct for any type A an equivalence

 
has-inverse(id A ) ' id A ∼ id A .

Note: We will use this fact in Exercise 15.6 to show that there are types for which
is-invertible(id A ) 6' is-equiv(id A ).
11.8 (a) Show that the type
∏ (t:∅) P(t)
is contractible for any P : ∅ → U .
(b) Show that for any type X the following are equivalent:
(i) the unique map ∅ → X is an equivalence.
(ii) The type Y X is contractible for any type Y.
11.9 Consider two types A and B.
(a) Show that the map
     
ev-inl-inr : ∏ (t:A+ B) P(t) → ∏ (x:A) P(inl( x )) × ∏ (y:B) P(inr(y))

given by f 7→ ( f ◦ inl, f ◦ inr) is an equivalence.

(b) Show that the following are equivalent for any type X equipped with maps
i : A → X and j : B → X:
(i) The map ind+ (i, j) : A + B → X is an equivalence.
(ii) For any type Y, the map

λ f . ( f ◦ i, f ◦ j) : ( X → Y ) → ( A → Y ) × ( B → Y )

is an equivalence.
11.10 (a) Show that the map  
∏ (t:1) P(t) → P(?)
given by λ f . f (?) is an equivalence.
(b) Consider a type X equipped with a point x : X. Show that the following are
equivalent:
(i) The map ind1 ( x ) : 1 → X is an equivalence (i.e., X is contractible).
(ii) For any type Y the map

λ f . f (x) : (X → Y) → Y

is an equivalence.
82 CHAPTER III. UNIVALENT MATHEMATICS

11.11 Consider a commuting triangle

h
A B

f g
X

with H : f ∼ g ◦ h.
(a) Show that if h has a section, then sec( g) is a retract of sec( f ).
(b) Show that if g has a retraction, then retr(h) is a retract of sec( f ).
11.12 Let ei : Ai ' Bi be an equivalence for every i : I. Show that the map
   
λ f . λi. ei ◦ f : ∏ (i:I ) Ai → ∏ (i:I ) Bi

is an equivalence.
11.13 Consider a diagram of the form

A B

f g
X

(a) Show that the type ∑(h:A→ B) f ∼ g ◦ h is equivalent to the type of families of
maps
∏ (x:X ) fib f ( x ) → fibg ( x ).
(b) Show that the type ∑(h:A' B) f ∼ g ◦ h is equivalent to the type of families of
equivalences
∏ (x:X ) fib f ( x ) ' fibg ( x ).
11.14 Consider a diagram of the form

A B
f g

X Y.
h

Show that the type ∑(i:A→ B) h ◦ f ∼ g ◦ i is equivalent to the type of families of

maps
∏ (x:X ) fib f ( x ) → fibg (h( x )).
11.15 Let A and B be sets. Show that type type A ' B of equivalences from A to B
is equivalent to the type A ∼ = B of isomorphisms from A to B, i.e., the type of
quadruples ( f , g, H, K ) consisting of

f :A→B
g:B→A
H : f ◦ g = idB
K : g ◦ f = id A .
12. THE UNIVALENCE AXIOM 83

11.16 Let B be a type family over A, and consider the maps

pr1 : ∑(x:A) B( x ) → A
 A
pr1 ◦ – : ∑(x:A) B( x ) → AA.

Construct equivalences
 
∏ (x:A) B ( x ) ' sec(pr1 ) ' fibpr1 ◦ – (id A ).

11.17 Suppose that A : I → U is a type family over a set I with decidable equality. Show
that    
∏ (i:I ) is-contr ( A i ) ↔ is-contr ∏ (i:I ) i .
A

11.18 Construct equivalences

Fin(nm ) ' (Fin(m) → Fin(n))

Fin(n!) ' (Fin(n) ' Fin(n)).

12 The univalence axiom

12.1 Equivalent forms of the univalence axiom
The univalence axiom characterizes the identity type of the universe. Roughly speaking,
it asserts that equivalent types are equal. It is considered to be an extensionality principle
for types.

Definition 12.1.1. The univalence axiom on a universe U is the statement that for any
A : U the family of maps

equiv-eq : ∏ ( B:U ) ( A = B) → ( A ' B).

that sends refl A to the identity equivalence id : A ' A is a family of equivalences. A

universe satisfying the univalence axiom is referred to as a univalent universe. If U is a
univalent universe we will write eq-equiv for the inverse of equiv-eq.

The following theorem is a special case of the fundamental theorem of identity types
(Theorem 9.2.2). Subsequently we will assume that any type is contained in a univalent
universe.

Theorem 12.1.2. The following are equivalent:

(i) The univalence axiom holds.

(ii) The type

∑( B:U ) A ' B
is contractible for each A : U .
84 CHAPTER III. UNIVALENT MATHEMATICS

(iii) The principle of equivalence induction holds: for every A : U and for every type family

P : ∏ ( B:U ) ( A ' B) → U ,

the map  
∏ ( B:U ) ∏ (e:A' B) P( B, e) → P( A, id A )

given by f 7→ f ( A, id A ) has a section.

12.2 Univalence implies function extensionality

One of the first applications of the univalence axiom was Voevodsky’s theorem that the
univalence axiom on a universe U implies function extensionality for types in U . The
proof uses the fact that weak function extensionality implies function extensionality.
We will also make use of the following lemma. Note that this statement was also part
of Exercise 11.3. That exercise is solved using function extensionality. Since our present
goal is to derive function extensionality from the univalence axiom, we cannot make use
of that exercise.

Lemma 12.2.1. For any equivalence e : X ' Y in a univalent universe U , and any type A, the
post-composition map
e ◦ – : ( A → X) → ( A → Y)
is an equivalence.

Proof. The statement is obvious for the identity equivalence id : X ' X. Therefore the
claim follows by equivalence induction, which is by Theorem 12.1.2 one of the equivalent
forms of the univalence axiom.

Theorem 12.2.2. For any universe U , the univalence axiom on U implies function extensionality
on U .

Proof. Note that by Theorem 11.1.2 it suffices to show that univalence implies weak
function extensionality, where we note that Theorem 11.1.2 also holds when it is restricted
to small types.
Suppose that B : A → U is a family of contractible types. Our goal is to show that the
product ∏ (x:A) B( x ) is contractible. Since each B( x ) is contractible, the projection map
pr1 : ∑(x:A) B( x ) → A is an equivalence by Exercise 8.6.

Now it follows by Lemma 12.2.1 that pr1 ◦ – is an equivalence. Consequently, it

follows from Theorem 8.3.6 that the fibers of
 
pr1 ◦ – : A → ∑(x:A) B( x ) → ( A → A)

are contractible. In particular, the fiber at id A is contractible. Therefore it suffices to show

that ∏ (x:A) B( x ) is a retract of ∑( f :A→∑(x:A) B(x)) pr1 ◦ f = id A . In other words, we will
construct
     
i r
∏ (x:A) B( x ) ∑( f :A→∑(x:A) B(x)) pr1 ◦ f = id A ∏ (x:A) B( x ) ,
12. THE UNIVALENCE AXIOM 85

and a homotopy r ◦ i ∼ id.

We define the function i by

i ( f ) :≡ (λx. ( x, f ( x )), reflid ).

To see that this definition is correct, we need to know that

λx. pr1 ( x, f ( x )) ≡ id.

This is indeed the case, by the η-rule for Π-types.

Next, we define the function r. Let h : A → ∑(x:A) B( x ), and let p : pr1 ◦ h = id.
Then we have the homotopy H :≡ htpy-eq( p) : pr1 ◦ h ∼ id. Then we have pr2 (h( x )) :
B(pr1 (h( x ))) and we have the identification H ( x ) : pr1 (h( x )) = x. Therefore we define r
by
r ((h, p), x ) :≡ tr B ( H ( x ), pr2 (h( x ))).
We note that if p ≡ reflid , then H ( x ) ≡ reflx . In this case we have the judgmental
equality r ((h, refl ), x ) ≡ pr2 (h( x )). Thus we see that r ◦ i ≡ id by another application of
the η-rule for Π-types.

12.3 Propositional extensionality and posets

Theorem 12.3.1. Propositions satisfy propositional extensionality: for any two propositions
P and Q, the canonical map

iff-eq : ( P = Q) → ( P ↔ Q)

that sends reflP to (id, id ) is an equivalence. It follows that the type Prop of propositions in U is
a set.

Note that for any P : Prop, we usually also write P for the underlying type of the
proposition P. If we would be more formal about it we would have to write pr1 ( P) for the
underlying type, since Prop is the Σ-type ∑(X:U ) is-prop( X ). In the following proof it is
clearer if we use the more formal notation pr1 ( P) for the underlying type of a proposition
P.

Proof. We note that the identity type P = Q is an identity type in Prop. However, since
is-prop( X ) is a proposition for any type X, it follows that the map

appr1 : ( P = Q) → (pr1 ( P) = pr1 ( Q))

is an equivalence. Now we observe that we have a commuting square

( P = Q) ( P ↔ Q)
appr1 '

(pr1 ( P) = pr1 ( Q)) equiv-eq

(pr1 ( P) ' pr1 ( Q))

Since the left, bottom, and right map are equivalences, it follows that the top map is an
equivalence.
86 CHAPTER III. UNIVALENT MATHEMATICS

Definition 12.3.2. A partially ordered set (poset) is a set P equipped with a relation

– ≤ – : P → ( P → Prop)

that is reflexive (for every x : P we have x ≤ x), transitive (for every x, y, z : P such that
x ≤ y and y ≤ z we have x ≤ z), and anti-symmetric (for every x, y : P such that x ≤ y
and y ≤ x we have x = y).

Remark 12.3.3. The condition that X is a set can be omitted from the definition of a poset.
Indeed, if X is any type that comes equipped with a Prop-valued ordering relation ≤
that is reflexive and anti-symmetric, then X is a set by Theorem 10.2.3.
Example 12.3.4. The type Prop is a poset, where the ordering relation is given by im-
plication: P is less than Q if P → Q. The fact that P → Q is a proposition is a special
case of Corollary 11.1.4. The relation P → Q is reflexive by the identity function, and
transitive by function composition. Moreover, the relation P → Q is anti-symmetric by
Theorem 12.3.1.
Example 12.3.5. The type of natural numbers comes equipped with at least two important
poset structures. The first is given by the usual ordering relation ≤, and the second is
given by the relation d | n that d divides n.

Theorem 12.3.6. For any poset P and any type X, the set P X is a poset. In particular the type
of subtypes of any type is a poset.

Proof. Let P be a poset with ordering ≤, and let X be a type. Then P X is a set by
Corollary 11.1.4. For any f , g : X → P we define

( f ≤ g) :≡ ∏ (x:X ) f ( x ) ≤ g( x ).

Reflexivity and transitivity follow immediately from reflexivity and transitivity of the
original relation. Moreover, by the anti-symmetry of the original relation it follows that

( f ≤ g ) × ( g ≤ f ) → ( f ∼ g ).

Therefore we obtain an identification f = g by function extensionality. The last claim

follows immediately from the fact that a subtype of X is a map X → Prop, and the fact
that Prop is a poset.

Exercises
12.1 (a) Use the univalence axiom to show that the type ∑( A:U ) is-contr( A) of all con-
tractible types in U is contractible.
(b) Use Corollaries 10.3.4 and 11.1.4 and Exercise 11.4 to show that if A and B are
(k + 1)-types, then the type A ' B is also a (k + 1)-type.
(c) Use univalence to show that the universe of k-types

U ≤k :≡ ∑(X:U ) is-trunck ( X )

is a (k + 1)-type, for any k ≥ −2.

(d) Show that U ≤−1 is not a proposition.
12. EXERCISES 87

(e) Show that (2 ' 2) ' 2, and conclude by the univalence axiom that the
universe of sets U ≤0 is not a set.
12.2 Use the univalence axiom to show that the type ∑( P:Prop) P is contractible.
12.3 Let A and B be small types.
(a) Construct an equivalence
 
( A → ( B → U )) ' ∑(S:U ) (S → A) × (S → B)

(b) We say that a relation R : A → ( B → U ) is functional if it comes equipped

with a term of type
 
is-function( R) :≡ ∏ (x:A) is-contr ∑(y:B) R( x, y)

For any function f : A → B, show that the graph of f

graph f : A → ( B → U )
given by graph f ( a, b) :≡ ( f ( a) = b) is a functional relation from A to B.
(c) Construct an equivalence
 
∑( R:A→( B→U )) is-function( R) ' ( A → B)

(d) Given a relation R : A → ( B → U ) we define the opposite relation

Rop : B → ( A → U )
by Rop (y, x ) :≡ R( x, y). Construct an equivalence
 
∑( R:A→( B→U )) is-function( R) × is-function( Rop ) ' ( A ' B).

12.4 (a) Show that is-decidable( P) is a proposition, for any proposition P.

(b) Show that classical-Prop is equivalent to 2.
12.5 Recall that U∗ is the universe of pointed types.
(a) For any ( A, a) and ( B, b) in U∗ , write ( A, a) '∗ ( B, b) for the type of pointed
equivalences from A to B, i.e.,
( A, a) '∗ ( B, b) :≡ ∑(e:A' B) e( a) = b.
Show that the canonical map

 
( A, a) = ( B, b) → ( A, a) ' ( B, b)

sending refl( A,a) to the pair (id, refla ), is an equivalence.

(b) Construct for any pointed type ( X, x0 ) an equivalence
 
∑( P:X →U ) P( x0 ) ' ∑(( A,a0 ):U∗ ) ( A, a0 ) →∗ ( X, x0 ).

12.6 Show that any subuniverse is closed under equivalences, i.e., show that there is a
map
( X ' Y ) → ( P( X ) → P(Y ))
for any subuniverse P : U → Prop, and any X, Y : U .
88 CHAPTER III. UNIVALENT MATHEMATICS

13 Groups in univalent mathematics

In this section we demonstrate a typical way to use the univalence axiom, showing
that isomorphic groups can be identified. This is an instance of the structure identity
principle, which is described in more detail in section 9.8 of [2]. We will see that in order
to establish the fact that isomorphic groups can be identified, it has to be part of the
definition of a group that its underlying type is a set. This is an important observation:
in many branches of algebra the objects of study are set-level structures1 .

13.1 Semi-groups and groups

We introduce the type of groups in two stages: first we introduce the type of semi-groups,
and then we introduce groups as semi-groups that possess further structure. It will turn
out that this further structure is in fact a property, and this fact will help us to prove that
isomorphic groups are equal.

Definition 13.1.1. A semi-group consists of a set G equipped with a term of type

has-associative-mul( G ), which is the type of pairs (µG , assocG ) consisting of a binary
operation
µG : G → (G → G)

and a homotopy

assocG : ∏ (x,y.z:G) µG (µG ( x, y), z) = µG ( x, µG (y, z)).

We write Semi-Group for the type of all semi-groups in U .

Definition 13.1.2. A semi-group G is said to be unital if it comes equipped with a unit

eG : G that satisfies the left and right unit laws

left-unitG : ∏ (y:G) µG (eG , y) = y

right-unitG : ∏ (x:G) µG ( x, eG ) = x.

We write is-unital( G ) for the type of such triples (eG , left-unitG , right-unitG ). Unital semi-
groups are also called monoids.

The unit of a semi-group is of course unique once it exists. In univalent mathematics

we express this fact by asserting that the type is-unital( G ) is a proposition for each semi-
group G. In other words, being unital is a property of semi-groups rather than structure
on it. This is typical for univalent mathematics: we express that a structure is a property
by proving that this structure is a proposition.

Lemma 13.1.3. For a semi-group G the type is-unital( G ) is a proposition.

1 A notable exception is that of categories, which are objects at truncation level 1, i.e., at the level of

groupoids. We will briefly introduce categories in §13.5. For more about categories we recommend Chapter 9
of [2].
13. GROUPS IN UNIVALENT MATHEMATICS 89

Proof. Let G be a semi-group. Note that since G is a set, it follows that the types of the
left and right unit laws are propositions. Therefore it suffices to show that any two terms
e, e0 : G satisfying the left and right unit laws can be identified. This is easy:
e = µG (e, e0 ) = e0 .
Definition 13.1.4. Let G be a unital semi-group. We say that G has inverses if it comes
equipped with an operation x 7→ x −1 of type G → G, satisfying the left and right inverse
laws
left-inv G : ∏ (x:G) µG ( x −1 , x ) = eG
right-inv G : ∏ (x:G) µG ( x, x −1 ) = eG .

We write is-group0 ( G, e) for the type of such triples (( – )−1 , left-inv G , right-inv G ), and we
write
is-group( G ) :≡ ∑(e:is-unital(G)) is-group0 ( G, e)
A group is a unital semi-group with inverses. We write Group for the type of all groups
in U .
Lemma 13.1.5. For any semi-group G the type is-group( G ) is a proposition.
Proof. We have already seen that the type is-unital( G ) is a proposition. Therefore it
suffices to show that the type is-group0 ( G, e) is a proposition for any e : is-unital( G ).
Since a semi-group G is assumed to be a set, we note that the types of the inverse
laws are propositions. Therefore it suffices to show that any two inverse operations
satisfying the inverse laws are homotopic.
Let x 7→ x −1 and x 7→ x̄ −1 be two inverse operations on a unital semi-group G, both
satisfying the inverse laws. Then we have the following identifications

x −1 = µ G ( e G , x −1 )
= µG (µG ( x̄ −1 , x ), x −1 )
= µG ( x̄ −1 , µG ( x, x −1 ))
= µG ( x̄ −1 , eG )
= x̄ −1
for any x : G. Thus the two inverses of x are the same, so the claim follows.
Example 13.1.6. An important class of examples consists of loop spaces x = x of a 1-type
X, for any x : X. We will write Ω ( X, x ) for the loop space of X at x. Since X is assumed
to be a 1-type, it follows that the type Ω ( X, x ) is a set. Then we have

reflx : Ω ( X, x )
inv : Ω ( X, x ) → Ω ( X, x )
concat : Ω ( X, x ) → (Ω ( X, x ) → Ω ( X, x )),
and these operations satisfy the group laws, since the group laws are just a special case
of the groupoid laws for identity types, constructed in §5.2.
90 CHAPTER III. UNIVALENT MATHEMATICS

Example 13.1.7. The type Z of integers can be given the structure of a group, with the
group operation being addition. The fact that Z is a set follows from Theorem 10.2.6
and Exercise 10.5. The group laws were shown in Exercise 7.11.
Example 13.1.8. Our last class of examples consists of the automorphism groups on sets.
Given a set X, we define
Aut( X ) :≡ ( X ' X ).
The group operation of Aut( X ) is just composition of equivalences, and the unit of
the group is the identity function. Note however, that although function composition
is strictly associative and satisfies the unit laws strictly, composition of equivalences
only satisfies the group laws up to identification because the proof that composites are
equivalences is carried along.
Important special cases of the automorphism groups are the symmetric groups
Sn :≡ Aut(Fin(n)).

13.2 Homomorphisms of semi-groups and groups

Definition 13.2.1. Let G and H be semi-groups. A homomorphismhomomorphism!of
semi-groups of semi-groups from G to H is a pair ( f , µ f ) consisting of a function f :
G → H between their underlying types, and a term
µ f : ∏ (x,y:G) f (µG ( x, y)) = µ H ( f ( x ), f (y))
witnessing that f preserves the binary operation of G. We will write
hom( G, H )
for the type of all semi-group homomorphisms from G to H.
Remark 13.2.2. Since it is a property for a function to preserve the multiplication of a
semi-group, it follows easily that equality of semi-group homomorphisms is equivalent
to the type of homotopies between their underlying functions. In particular, it follows
that the type of homomorphisms of semi-groups is a set.
Remark 13.2.3. The identity homomorphism on a semi-group G is defined to be the pair
consisting of

id : G → G
λx. λy. reflxy : ∏ (x,y:G) xy = xy.
Let f : G → H and g : H → K be semi-group homomorphisms. Then the compos-
ite function g ◦ f : G → K is also a semi-group homomorphism, since we have the
identifications
g( f ( xy)) g( f ( x ) f (y)) g( f ( x )) g( f (y)).

Since the identity type of semi-group homomorphisms is equivalent to the type of

homotopies between semi-group homomorphisms it is easy to see that semi-group
homomorphisms satisfy the laws of a category, i.e., that we have the identifications

id ◦ f = f
13. GROUPS IN UNIVALENT MATHEMATICS 91

g ◦ id = g
(h ◦ g) ◦ f = h ◦ ( g ◦ f )

for any composable semi-group homomorphisms f , g, and h. Note, however that these
equalities are not expected to hold judgmentally, since preservation of the semi-group
operation is part of the data of a semi-group homomorphism.

Definition 13.2.4. Let G and H be groups. A homomorphism of groups from G to H is

defined to be a semi-group homomorphism between their underlying semi-groups. We
will write
hom( G, H )
for the type of all group homomorphisms from G to H.

Remark 13.2.5. Since a group homomorphism is just a semi-group homomorphism be-

tween the underlying semi-groups, we immediately obtain the identity homomorphism,
composition, and the category laws are satisfied.

13.3 Isomorphic semi-groups are equal

Definition 13.3.1. Let h : hom( G, H ) be a homomorphism of semi-groups. Then h is said
to be an isomorphism if it comes equipped with a term of type is-iso(h), consisting of
triples (h−1 , p, q) consisting of a homomorphism h−1 : hom( H, G ) of semi-groups and
identifications
p : h−1 ◦ h = idG and q : h ◦ h−1 = id H
witnessing that h−1 satisfies the inverse lawsWe write G ∼
= H for the type of all isomor-
phisms of semi-groups from G to H, i.e.,

G∼
= H :≡ ∑(h:hom(G,H )) ∑(k:hom( H,G)) (k ◦ h = idG ) × (h ◦ k = id H ).

If f is an isomorphism, then its inverse is unique. In other words, being an isomor-

phism is a property.

Lemma 13.3.2. For any semi-group homomorphism h : hom( G, H ), the type

is-iso(h)

is a proposition. It follows that the type G ∼

= H is a set for any two semi-groups G and H.

Proof. Let k and k0 be two inverses of h. In Remark 13.2.2 we have observed that the
type of semi-group homomorphisms between any two semi-groups is a set. Therefore it
follows that the types h ◦ k = id and k ◦ h = id are propositions, so it suffices to check
that k = k0 . In Remark 13.2.2 we also observed that the equality type k = k0 is equivalent
to the type of homotopies k ∼ k0 between their underlying functions. We construct a
homotopy k ∼ k0 by the usual argument:

k(y) k (h(k0 (y)) k 0 ( y ).

92 CHAPTER III. UNIVALENT MATHEMATICS

Lemma 13.3.3. A semi-group homomorphism h : hom( G, H ) is an isomorphism if and only if

its underlying map is an equivalence. Consequently, there is an equivalence
(G ∼
= H ) ' ∑(e:G' H ) ∏ (x,y:G) e(µG ( x, y)) = µ H (e( x ), e(y))
Proof. If h : hom( G, H ) is an isomorphism, then the inverse semi-group homomorphism
also provides an inverse of the underlying map of h. Thus we obtain that h is an
equivalence. The standard proof showing that if the underlying map f : G → H of a
group homomorphism is invertible then its inverse is again a group homomorphism
also works in type theory.
Definition 13.3.4. Let G and H be a semi-groups. We define the map
iso-eq : ( G = H ) → ( G ∼
= H)
by path induction, taking reflG to isomorphism idG .
Theorem 13.3.5. The map
iso-eq : ( G = H ) → ( G ∼
= H)
is an equivalence for any two semi-groups G and H.
Proof. By the fundamental theorem of identity types Theorem 9.2.2 it suffices to show
that the total space
∑(G0 :Semi-Group) G ∼
= G0
is contractible. Since the type of isomorphisms from G to G 0 is equivalent to the type of
equivalences from G to G 0 it suffices to show that the type

∑(G0 :Semi-Group) ∑(e:G'G0 ) ∏ (x,y:G) e(µG ( x, y)) = µG0 (e( x ), e(y)))

is contractible2 . Since Semi-Group is the Σ-type

∑(G0 :Set) has-associative-mul( G 0 ),

it suffices to show that the types

∑(G0 :Set) G ' G 0

∑(µ0 :has-associative-mul(G)) ∏ (x,y:G) µG ( x, y) = µ0 ( x, y)
is contractible. The first type is contractible by the univalence axiom. The second type is
contractible by function extensionality.
Corollary 13.3.6. The type Semi-Group is a 1-type.
Proof. It is straightforward to see that the type of group isomorphisms G ∼
= H is a set,
for any two groups G and H.
2 In order to show that a type of the form
∑(( x,y):∑(x:A) B( x)) ∑(z:C( x)) D ( x, y, z)

is contractible, a useful strategy is to first show that the type ∑( x:A) C ( x ) is contractible. Once this is
established, say with center of contraction ( x0 , z0 ), it suffices to show that the type ∑(y:B( x0 )) D ( x0 , y, z0 ) is
contractible.
13. GROUPS IN UNIVALENT MATHEMATICS 93

13.4 Isomorphic groups are equal

Analogously to the map iso-eq of semi-groups, we have a map iso-eq of groups. Note,
however, that the domain of this map is now the identity type G = H of the groups G
and H, so the maps iso-eq of semi-groups and groups are not exactly the same maps.
Definition 13.4.1. Let G and H be groups. We define the map

iso-eq : ( G = H ) → ( G ∼
= H)
by path induction, taking reflG to the identity isomorphism id : G ∼
= G.
Theorem 13.4.2. For any two groups G and H, the map

iso-eq : ( G = H ) → ( G ∼
= H)
is an equivalence.
Proof. Let G and H be groups, and write UG and UH for their underlying semi-groups,
respectively. Then we have a commuting triangle
appr1
(G = H ) (UG = UH )

iso-eq iso-eq
(G ∼
= H)

Since being a group is a property of semi-groups it follows that the projection map
Group → Semi-Group forgetting the unit and inverses, is an embedding. Thus the top
map in this triangle is an equivalence. The map on the right is an equivalence by
Theorem 13.3.5, so the claim follows by the 3-for-2 property.
Corollary 13.4.3. The type of groups is a 1-type.

13.5 Categories in univalent mathematics

In our proof of the fact that isomorphic groups are equal we have made extensive use
of the notion of group homomorphism. What we have shown, in fact, is that there is a
category of groups which is Rezk complete in the sense that the type of isomorphisms
between two objects is equivalent to the type of identifications between those objects. In
this final section we briefly introduce the notion of Rezk complete category. There are
many more examples of categories, such as the categories of rings, or modules over a
ring.
Definition 13.5.1. A pre-category C consists of
(i) A type A of objects.

(ii) For every two objects x, y : A a set

hom( x, y)

of morphisms from x to y.
94 CHAPTER III. UNIVALENT MATHEMATICS

(iii) For every object x : A an identity morphism

id : hom( x, x )

(iv) For every two morphisms f : hom( x, y) and g : hom(y, z), a morphism
g ◦ f : hom( x, z)
called the composition of f and g.
(v) the following terms

left-unitC : id ◦ f = f
right-unitC : g ◦ id = g
assocC : (h ◦ g) ◦ f = h ◦ ( g ◦ f )
witnessing that the category laws are satisfied.
Example 13.5.2. Since the type X → Y of functions between sets is again a set, we have a
pre-category of sets.
Example 13.5.3. By Remarks 13.2.3 and 13.2.5 we have pre-categories of semi-groups and
of groups.
Example 13.5.4. A pre-category satisfying the condition that every hom-set is a proposi-
tion is a preorder.
Definition 13.5.5. Given a pre-category C , a morphism f : hom( x, y) is said to be an
isomorphism if there exists a morphism g : hom(y, x ) such that

g ◦ f = id
f ◦ gid.
We will write iso( x, y) for the type of all isomorphisms in C from x to y.
Remark 13.5.6. Just as in the case for semi-groups and groups, the condition that f :
hom( x, y) is an isomorphism is a property of f .
Definition 13.5.7. A pre-category C is said to be Rezk-complete if the canonical map
( x = y) → iso( x, y)
is an equivalence for any two objects x and y of C . Rezk-complete pre-categories are also
called categories.
Example 13.5.8. The pre-category of sets is Rezk complete by the univalence axiom, so it
is a category.
Example 13.5.9. The pre-categories of semi-groups and groups are Rezk-complete. There-
fore they form categories.
Example 13.5.10. A pre-order is Rezk-complete if and only if it is anti-symmetric. In other
words, a poset is precisely a category for which all the hom-sets are propositions. Thus,
we see that the anti-symmetry axiom can be seen as a univalence axiom for pre-orders.
13. EXERCISES 95

Exercises
13.1 Let X be a set. Show that the map

equiv-eq : ( X = X ) → ( X ' X )

is a group isomorphism.
13.2 (a) Consider a group G. Show that the function

µG : G → (G ' G)

is an injective group homomorphism.

(b) Consider a pointed type A. Show that the concatenation function

concat : Ω ( A) → (Ω ( A) ' Ω ( A))

is an embedding.
13.3 Let f : hom( G, H ) be a group homomorphism. Show that f preserves units and
inverses, i.e., show that

f (eG ) = e H
f ( x −1 ) = f ( x ) −1 .

13.4 Give a direct proof and a proof using the univalence axiom of the fact that all semi-
group isomorphisms between unital semi-groups preserve the unit. Conclude that
isomorphic monoids are equal.
13.5 Consider a monoid M with multiplication µ : M → ( M → M) and unit e. Write

µ̄ :≡ fold-list(e, µ) : list( M ) → M

for the iterated multiplication operation (see Exercise 4.8). Show that the square

flatten-list( M )
list(list( M)) list( M )
list(µ̄) µ̄

list( M) µ̄
M

commutes.
13.6 Construct the category of posets.

14 The circle
We have seen inductive types, in which we describe a type by its constructors and an
induction principle that allows us to construct sections of dependent types. Inductive
types are freely generated by their constructors, which describe how we can construct
their terms.
However, many familiar constructions in algebra involve the construction of algebras
by generators and relations. For example, the free abelian group with two generators is
described as the group with generators x and y, and the relation xy = yx.
96 CHAPTER III. UNIVALENT MATHEMATICS

In this chapter we introduce higher inductive types, where we follow a similar idea:
to allow in the specification of inductive types not only point constructors, but also path
constructors that give us relations between the point constructors. The ideas behind the
definition of higher inductive types are introduced by studying the simplest non-trivial
example: the circle.

14.1 The induction principle of the circle

The circle is defined as a higher inductive type S1 that comes equipped with

base : S1
loop : base = base.

Just like for ordinary inductive types, the induction principle for higher inductive types
provides us with a way of constructing sections of dependent types. However, we need
to take the path constructor loop into account in the induction principle.
By applying a section f : ∏ (x:S1 ) P( x ) to the base point of the circle, we obtain a term
f (base) : P(base). Moreover, using the dependent action on paths of f of Definition 5.4.2
we also obtain for any dependent function f : ∏ (x:S1 ) P( x ) a path

apd f (loop) : tr P (loop, f (base)) = f (base)

in the fiber P(base).

Definition 14.1.1. Let P be a type family over the circle. The dependent action on
generators is the map
   
dgenS1 : ∏ (x:S1 ) P( x ) → ∑(y:P(base)) tr P (loop, y) = y (14.1)

given by dgenS1 ( f ) :≡ ( f (base), apd f (loop)).

We now give the full specification of the circle.

Definition 14.1.2. The circle is a type S1 that comes equipped with

base : S1
loop : base = base,

and satisfies the induction principle of the circle, which provides for each type family
P over S1 a map
   
indS1 : ∑(y:P(base)) tr P (loop, y) = y → ∏ (x:S1 ) P( x ) ,

and a homotopy witnessing that indS1 is a section of dgenS1

compS1 : dgenS1 ◦ indS1 ∼ id

for the computation rule.

14. THE CIRCLE 97

Remark 14.1.3. The type of identifications (y, p) = (y0 , p0 ) in the type

∑(y:P(base)) tr P (loop, y) = y

is equivalent to the type of pairs (α, β) consisting of an identification α : y = y0 , and an

identification β witnessing that the square

aptr
P (loop)
(α)
tr P (loop, y) tr P (loop, y0 )
p p0

y α y0

commutes. Therefore it follows from the induction principle of the circle that for
any (y, p) : ∑(y:P(base)) tr P (loop, y) = y, there is a dependent function f : ∏ (x:S1 ) P( x )
equipped with an identification

α : f (base) = y,

and an identification β witnessing that the square

aptr
P (loop)
(α)
tr P (loop, f (base)) tr P (loop, y)
apd f (loop) p

f (base) α y

commutes.

14.2 The (dependent) universal property of the circle

Our goal is now to use the induction principle of the circle to derive the universal
property of the circle. This universal property states that, for any type X the canonical
map    
S1 → X → ∑(x:X ) x = x

given by f 7→ ( f (base), ap f (loop)) is an equivalence. It turns out that it is easier to prove

the dependent universal property first. The dependent universal property states that
for any type family P over the circle, the canonical map
   
∏ (x:S )
1 P ( x ) → ∑(y:P(base)) P
tr ( loop, y ) = y

given by f 7→ ( f (base), apd f (loop)) is an equivalence.

Theorem 14.2.1. For any type family P over the circle, the map
   
∏ (x:S1 ) P( x ) → ∑(y:P(base)) tr P (loop, y) = y

given by f 7→ ( f (base), apd f (loop)) is an equivalence.

98 CHAPTER III. UNIVALENT MATHEMATICS

Proof. By the induction principle of the circle we know that the map has a section, i.e.,
we have
   
indS1 : ∑(y:P(base)) tr P (loop, y) = y → ∏ (x:S1 ) P( x )

compS1 : dgenS1 ◦ indS1 ∼ id

Therefore it remains to construct a homotopy

indS1 ◦ dgenS1 ∼ id.

Thus, for any f : ∏ (x:S1 ) P( x ) our task is to construct an identification

indS1 (dgenS1 ( f )) = f .

By function extensionality it suffices to construct a homotopy

∏ (x:S1 ) indS1 (dgenS1 ( f ))( x ) = f ( x ).

We proceed by the induction principle of the circle using the family of types Eg, f ( x ) :≡
g( x ) = f ( x ) indexed by x : S1 , where g is the function

g :≡ indS1 (dgenS1 ( f )).

Thus, it suffices to construct

α : g(base) = f (base)
β : tr Eg, f (loop, α) = α.

An argument by path induction on p yields that

   
apdg ( p)  r = aptrP ( p) (q)  apd f ( p) → tr Eg, f ( p, q) = r ,

for any f , g : ∏ (x:X ) P( x ) and any p : x = x 0 , q : g( x ) = f ( x ) and r : g( x 0 ) = f ( x 0 ).

Therefore it suffices to construct an identification α : g(base) = f (base) equipped with
an identification β witnessing that the square

aptr
P (loop)
(α)
tr P (loop, g(base)) tr P (loop, f (base))
apdg (loop) apd f (loop)

g(base) α f (base)”

commutes. Notice that we get exactly such a pair (α, β) from the computation rule of the
circle, by Remark 14.1.3.

As a corollary we obtain the following uniqueness principle for dependent functions

defined by the induction principle of the circle.
14. THE CIRCLE 99

Corollary 14.2.2. Consider a type family P over the circle, and let

y : P(base)
p : tr P (loop, y) = y.

Then the type of functions f : ∏ (x:S1 ) P( x ) equipped with an identification

α : f (base) = y

and an identification β witnessing that the square

aptr
P (loop)
(α)
tr P (loop, f (base)) tr P (loop, y)
apd f (loop) p

f (base) α y

commutes, is contractible.

Now we use the dependent universal property to derive the ordinary universal
property of the circle. It would be tempting to say that it is a direct corollary, but we
need to address the transport that occurs in the dependent universal property.

Theorem 14.2.3. For each type X, the action on generators

genS1 : (S1 → X ) → ∑(x:X ) x = x

given by f 7→ ( f (base), ap f (loop)) is an equivalence.

Proof. We prove the claim by constructing a commuting triangle

( S1 → X )
genS1 dgenS1

   
∑(x:X ) x = x ' ∑(x:X ) trconstX (loop, x ) = x

in which the bottom map is an equivalence. Indeed, once we have such a triangle, we
use the fact from Theorem 14.2.1 that dgenS1 is an equivalence to conclude that genS1 is
an equivalence.
To construct the bottom map, we first observe that for any constant type family constB
over a type A, any p : a = a0 in A, and any b : B, there is an identification

tr-constB ( p, b) = b.

This identification is easily constructed by path induction on p. Now we construct the

bottom map as the induced map on total spaces of the family of maps

l 7→ tr-constX (loop, x )  l,
100 CHAPTER III. UNIVALENT MATHEMATICS

indexed by x : X. Since concatenating by a path is an equivalence, it follows by Theo-

rem 9.1.3 that the induced map on total spaces is indeed an equivalence.
To show that the triangle commutes, it suffices to construct for any f : S1 → X an
identification witnessing that the triangle

tr-constX (loop, f (base))

trconstX (loop, f (base)) f (base)

apd f (loop) ap f (loop)

f (base)

commutes. This again follows from general considerations: for any f : A → B and any
p : a = a0 in A, the triangle

tr-constB ( p, f ( a))
trconstB ( p, f ( a)) f ( a)

apd f ( p) ap f ( p)
f ( a0 )

commutes by path induction on p.

Corollary 14.2.4. For any loop l : x = x in a type X, the type of maps f : S1 → X equipped
with an identification
α : f (base) = x

and an identification β witnessing that the square

α
f (base) x
ap f (loop) l

f (base) α x

commutes, is contractible.

14.3 Multiplication on the circle

One way the circle arises classically, is as the set of complex numbers at distance 1 from
the origin. It is an elementary fact that | xy| = | x ||y| for any two complex numbers
x, y ∈ C, so it follows that when we multiply two complex numbers that both lie on the
unit circle, then the result lies again on the unit circle. Thus, using complex multiplication
we see that there is a multiplication operation on the circle. And there is a shadow of
this operation in type theory, even though our circle arises in a very different way!

Definition 14.3.1. We define a binary operation

mulS1 : S1 → (S1 → S1 ).
14. THE CIRCLE 101

Construction. Using the universal property of the circle, we define mulS1 as the unique
map S1 → (S1 → S1 ) equipped with an identification

base-mulS1 : mulS1 (base) = id

and an identification loop-mulS1 witnessing that the square

base-mulS1
mulS1 (base) id
apmul (loop) eq-htpy( H )
S1

mulS1 (base) id
base-mulS1

commutes. Note that in this square we have a homotopy H : id ∼ id, which is not yet
defined. We use the dependent universal property of the circle with respect to the family
Eid,id given by
Eid,id ( x ) :≡ ( x = x ),

to define H as the unique homotopy equipped with an identification

α : H (base) = loop

and an identification β witnessing that the square

aptr
Eid,id (loop)
(α)
tr Eid,id (loop, H (base)) tr Eid,id (loop, loop)
apd H (loop) γ

H (base) α loop

commutes. Now it remains to define the path γ : tr Eid,id (loop, loop) = loop in the above
square. To proceed, we first observe that a simple path induction argument yields a
function    
p  r = q  p → tr Eid,id ( p, q) = r ,

for any p : base = x, q : base = base and r : x = x. In particular, we have a function

   
loop  loop = loop  loop → tr Eid,id (loop, loop) = loop .

Now we apply this function to reflloop  loop to obtain the desired identification

γ : tr Eid,id (loop, loop) = loop.

Remark 14.3.2. In the definition of H : id ∼ id above, it is important that we didn’t choose

H to be htpy-refl. If we had done so, the resulting operation would be homotopic to
x, y 7→ y, which is clearly not what we had in mind with the multiplication operation on
the circle. See also Exercise 14.3.
102 CHAPTER III. UNIVALENT MATHEMATICS

The left unit law mulS1 (base, x ) = x holds by the computation rule of the universal
property. More precisely, we define

left-unitS1 :≡ htpy-eq(base-mulS1 ).

For the right unit law, however, we need to give a separate argument that is surprisingly
involved, because all the aspects of the definition of mulS1 will come out and play their
part.

Theorem 14.3.3. The multiplication operation on the circle satisfies the right unit law, i.e., we
have
mulS1 ( x, base) = x
for any x : S1 .

Proof. The proof is by induction on the circle. In the base case we use the left unit law

left-unitS1 (base) : mulS1 (base, base) = base.

Thus, it remains to show that

tr P (loop, left-unitS1 (base)) = left-unitS1 (base),

where P is the family over the circle given by

P( x ) :≡ mulS1 ( x, base) = x.

Now we observe that there is a function

   
htpy-eq(apmul 1 ( p))(base)  r = q  p → tr P ( p, q) = r ,
S

for any

p : base = x
q : mulS1 (base, base) = base
r : mulS1 ( x, base) = x.

Thus we see that, in order to construct an identification

tr P (loop, left-unitS1 ) = left-unitS1 ,

it suffices to show that the square

left-unitS1 (base)
mulS1 (base, base) base
htpy-eq(apmul (loop))(base) loop
S1

mulS1 (base, base) base

left-unitS1 (base)
14. EXERCISES 103

commutes. Now we note that we have an identification H (base) = loop. It is indeed at

this point, where it is important that H is not the trivial homotopy, because now we can
proceed by observing that the above square commutes if and only if the square

htpy-eq(base-mulS1 )(base)
mulS1 (base, base) base
htpy-eq(apmul (loop))(base) H (base)
S1

mulS1 (base, base) base

htpy-eq(base-mulS1 )(base)

commutes. The commutativity of this square easily follows from the identification
loop-mulS1 constructed in Definition 14.3.1.

Exercises
14.1 Let P : S1 → Prop be a family of propositions over the circle. Show that

P(base) → ∏ (x:S1 ) P( x ).

In this sense the circle is connected.

14.2 Show that
∏ (x,y:S1 ) ¬¬( x = y).
14.3 Show that for any type X and any x : X, the map

indS1 ( x, reflx ) : S1 → X

is homotopic to the constant map constx .

14.4 (a) Show that for any x : S1 , both functions

mulS1 ( x, – ) and mulS1 ( –, x )

are equivalences.
(b) Show that the function

mulS1 : S1 → (S1 → S1 )

is an embedding. Compare this fact with Exercise 13.2.

(c) Show that multiplication on the circle is associative and commutative.
14.5 (a) Show that a type X is a set if and only if the map

λx. λt. x : X → (S1 → X )

is an equivalence.
(b) Show that a type X is a set if and only if the map

λ f . f (base) : (S1 → X ) → X

is an equivalence.
104 CHAPTER III. UNIVALENT MATHEMATICS

15 The fundamental cover of the circle

In this lecture we show that the loop space of the circle is equivalent to Z by constructing
the universal cover of the circle as an application of the univalence axiom.

15.1 Families over the circle

The type of small families over S1 is just the function type S1 → U , so in fact we may use
the universal property of the circle to construct small dependent types over the circle. By
the universal property, small type families over S1 are equivalently described as pairs
( X, p) consisting of a type X : U and an identification p : X = X. This is where the
univalence axiom comes in. By the map

eq-equiv X,X : ( X ' X ) → ( X = X )

it suffices to provide an equivalence X ' X.

Definition 15.1.1. Consider a type X and every equivalence e : X ' X. We will construct
a dependent type D( X, e) : S1 → U with an equivalence x 7→ xD : X ' D( X, e, base) for
which the square
'
X D( X, e, base)
e trD(X,e) (loop)

X ' D( X, e, base)

commutes. We also write d 7→ d X for the inverse of this equivalence, so that the relations

( xD ) X = x (e( x )D ) = trD(X,e) (loop, xD )

(d X )D = d (trD(X,e) (d))X = e(d X )

hold.
The type ∑(X:U ) X ' X is also called the type of descent data for the circle.

Construction. An easy path induction argument reveals that

equiv-eq(apP (loop)) = tr P (loop)

for each dependent type P : S1 → U . Therefore we see that the triangle

( S1 → U )
genS1 descS1

∑(X:U ) X = X tot (λX. equiv-eqX,X )

∑(X:U ) X ' X

commutes, where the map descS1 is given by P 7→ ( P(base), tr P (loop)) and the bottom
map is an equivalence by the univalence axiom and Theorem 9.1.3. Now it follows
by the 3-for-2 property that descS1 is an equivalence, since genS1 is an equivalence by
15. THE FUNDAMENTAL COVER OF THE CIRCLE 105

Theorem 14.2.3. This means that for every type X and every e : X ' X there is a type
family D( X, e) : S1 → U such that

(D( X, e, base), trD(X,e) (loop)) = ( X, e).

Equivalently, we have p : D( X, e, base) = X and tr( p, trD(X,e) (loop)) = e. Thus, we obtain
equiv-eq( p) : D( X, e, base) ' X, for which the square
equiv-eq( p)
D( X, e, base) X
trD(X,e) (loop) e

D( X, e, base) X
equiv-eq( p)

commutes.

15.2 The fundamental cover of the circle

The fundamental cover of the circle is a family of sets over the circle with contractible
total space. Classically, the fundamental cover is described as a map R → S1 that winds
the real line around the circle. In homotopy type theory there is no analogue of such a
construction.
Recall from Exercise 7.6 that the successor function succ : Z → Z is an equivalence.
Its inverse is the predecessor function defined in Exercise 4.4.
Definition 15.2.1. The fundamental cover of the circle is the dependent type ES1 :≡
D(Z, succ) : S1 → U .
Remark 15.2.2. The fundamental cover of the circle comes equipped with an equivalence

e : Z ' ES1 (base)

and a homotopy witnessing that the square

e
Z ES1 (base)
succ trE (loop)
S1

Z e ES1 (base)

commutes.
For convenience, we write k E for the term e(k ) : ES1 (base), for any k : Z.
The picture of the fundamental cover is that of a helix over the circle. This picture
emerges from the path liftings of loop in the total space. The segments of the helix
connecting k to k + 1 in the total space of the helix, are constructed in the following
lemma.
Lemma 15.2.3. For any k : Z, there is an identification

segment-helixk : (base, k E ) = (base, succ(k )E )

in the total space ∑(t:S1 ) E (t).

106 CHAPTER III. UNIVALENT MATHEMATICS

Proof. By Theorem 7.3.4 it suffices to show that

∏ (k:Z) ∑(α:base=base) trE (α, k E ) = succ(k )E .

We just take α :≡ loop. Then we have trE (α, k E ) = succ(k )E by the commuting square
provided in the definition of E .

15.3 Contractibility of general total spaces

Consider a type X, a family P over X, and a term c : ∑(x:X ) P( x ), and suppose our goal
is to construct a contraction
∏ (t:∑(x:X) P(x)) c = t.
Of course, the first step is to apply the induction principle of Σ-types, so it suffices to
construct a term of type
∏ (x:X ) ∏ (y:P(x)) c = ( x, y).
In the case where P is the fundamental cover of the circle, we are given an equivalence
e : Z ' E (base). Using this equivalence, we obtain an equivalence
   
∏ (y:E (y)) c = (base, y) → ∏ (k:Z) c = (base, k E ) .

More generally, if we are given an equivalence e : F ' P( x ) for some x : X, then we have
an equivalence    
∏ (y:P(x)) c = ( x, y) → ∏ (y:F) c = ( x, e(y)) (15.1)

by precomposing with the equivalence e. Therefore we can construct a term of type

∏ (y:P(x)) c = ( x, y) by constructing a term of type ∏ (y:F) c = ( x, e(y)).
Furthermore, if we consider a path p : x = x 0 in X and a commuting square
e
F P( x )
f tr P ( p)
e0
F0 P( x0 )

where e, e0 , and f are all equivalences, then we obtain a function

   
ψ : ∏ (y:F) c = ( x, e(y)) → ∏ (y0 :F0 ) c = ( x, e0 (y0 )) .

The function ψ is constructed as follows. Given h : ∏ (y:F) c = ( x, e(y)) and y0 : F 0 we

have the path h( f −1 (y0 )) : c = ( x, e( f −1 (y0 ))). Moreover, writing G for the homotopy
f ◦ f −1 ∼ id, we have the path

H ( f −1 (y0 )) ape0 ( G (y0 ))

tr P ( p, e( f −1 (y0 ))) e0 ( f ( f −1 (y0 ))) e 0 ( y 0 ).

From this concatenated path we obtain the path

eq-pair( p,H ( f −1 (y0 ))  ape0 ( G (y0 )))

( x, e( f −1 (y0 ))) ( x 0 , e0 (y0 )).
15. THE FUNDAMENTAL COVER OF THE CIRCLE 107

Now we define the function ψ by

h 7→ λy0 . h( f −1 (y0 ))  eq-pair( p, H ( f −1 (y0 ))  ape0 ( G (y0 ))).

Note that ψ is an equivalence, since it is given as precomposition by the equivalence f −1 ,

followed by postcomposition by concatenation, which is also an equivalence. Now we
state the main technical result of this section, which will help us prove the contractibility
of the total space of the fundamental cover of the circle by computing transport in the
family x 7→ ∏ (y:P(x)) c = ( x, y).

Definition 15.3.1. Consider a path p : x = x 0 in X and a commuting square

e
F P( x )
f tr P ( p)
e0
F0 P( x0 )

with H : e0 ◦ f tr P ( p) ◦ e, where e, e0 , and f are all equivalences. Then there is for any
y : F an identification

segment-tot(y) : ( x, e(y)) = ( x 0 , e0 ( f (y)))

defined as segment-tot(y) :≡ eq-pair( p, H (y)−1 ).

Lemma 15.3.2. Consider a path p : x = x 0 in X and a commuting square

e
F P( x )
f tr P ( p)
e0
F0 P( x0 )

with H : e0 ◦ f tr P ( p) ◦ e, where e, e0 , and f are all equivalences. Furthermore, let

h : ∏ (y:F) c = ( x, e(y))
h0 : ∏ (y0 :F0 ) c = ( x 0 , e0 (y0 )).

Then there is an equivalence

   
∏ (y:F) h0 ( f (y)) = h(y)  segment-tot(y) ' trC ( p, ϕ(h)) = ϕ0 (h0 ) .

Proof. We first note that we have a commuting square

– ◦e
∏ (y:B(x)) c = ( x, y) ∏ (y:F) c = ( x, e(y))
trC ( p) ψ

∏ (y0 :B(x0 )) c = ( x 0 , y0 ) ∏ (y0 :F0 ) c = ( x 0 , e0 (y0 ))

– ◦e0
108 CHAPTER III. UNIVALENT MATHEMATICS

where ψ(h0 ) = λy. h0 ( f (y))  segment-tot(y)−1 . All the maps in this square are equiva-
lences. In particular, the inverses of the top and bottom maps are ϕ and ϕ0 , respectively.
The claim follows from this observation, but we will spell out the details.
Since any equivalence is an embedding, we see immediately that the type trC ( p)( ϕ(h)) =
ϕ (h0 ) is equivalent to the type
0

ψ(trC ( p)( ϕ(h)) ◦ e0 ) = ψ( ϕ0 (h0 ) ◦ e0 ).

By the commutativity of the square, the left hand side is h. The right hand side is ψ(h0 ).
Therefore it follows that
   
trC ( p)( ϕ(h)) = ϕ0 (h0 ) ' h = λy. h0 ( f (y))  segment-tot(y)−1
 
' h0 ◦ f ∼ (λy. h(y)  segment-tot(y) .

Applying these observations to the fundamental cover of the circle, we obtain the
following lemma that we will use to prove that the total space of E is contractible.

Corollary 15.3.3. In order to show that the total space of E is contractible, it suffices to construct
a function
h : ∏ (k:Z) (base, 0E ) = (base, k E )
equipped with a homotopy

H : ∏ (k:Z) h(succ(k )E ) = h(k )  segment-helix(k ).

In the next section we establish the dependent universal property of the integers,
which we will use with Corollary 15.3.3 to show that the total space of the fundamental
cover is contractible.

15.4 The dependent universal property of the integers

Lemma 15.4.1. Let B be a family over Z, equipped with a term b0 : B(0), and an equivalence

ek : B(k ) ' B(succ(k ))

for each k : Z. Then there is a dependent function f : ∏ (k:Z) B(k ) equipped with identifications
f (0) = b0 and
f (succ(k )) = ek ( f (k ))
for any k : Z.

Proof. The map is defined using the induction principle for the integers, stated in
Lemma 4.5.3. First we take

f (−1) :≡ e−1 (b0 )

f (0) :≡ b0
f (1) :≡ e(b0 ).
15. THE FUNDAMENTAL COVER OF THE CIRCLE 109

For the induction step on the negative integers we use

−1
(S(n)) ∏ (n:N)
λn. eneg : B(neg(n)) → B(neg(S(n)))
For the induction step on the positive integers we use
λn. e(pos(n)) : ∏ (n:N) B(pos(n)) → B(pos(S(n))).
The computation rules follow in a straightforward way from the computation rules of
Z-induction and the fact that e−1 is an inverse of e.
Example 15.4.2. For any type A, we obtain a map f : Z → A from any x : A and any
equivalence e : A ' A, such that f (0) = x and the square
f
Z A
succ e

Z A
f

commutes. In particular, if we take A ≡ ( x = x ) for some x : X, then for any p : x = x

we have the equivalence λq. p  q : ( x = x ) → ( x = x ). This equivalence induces a map
k 7 → p k : Z → ( x = x ),
for any p : x = x. This induces the degree k map on the circle
deg(k ) : S1 → S1 ,
for any k : Z, see Exercise 15.2.
In the following theorem we show that the dependent function constructed in
Lemma 15.4.1 is unique.
Theorem 15.4.3. Consider a type family B : Z → U equipped with b : B(0) and a family of
equivalences
e : ∏ (k:Z) B(k ) ' B(succ(k )).
Then the type
∑( f :∏ (k:Z) B(k)) ( f (0) = b) × ∏ (k:Z) f (succ(k)) = ek ( f (k ))
is contractible.
Proof. In Lemma 15.4.1 we have already constructed a term of the asserted type. There-
fore it suffices to show that any two terms of this type can be identified. Note that the
type ( f , p, H ) = ( f 0 , p0 , H 0 ) is equivalent to the type
∑(K: f ∼ f 0 ) (K (0) = p  ( p0 )−1 ) × ∏ (k:Z) K (succ(k )) = ( H (k )  apek (K (k)))  H 0 (k )−1 .
We obtain a term of this type by applying Lemma 15.4.1 to the family C over Z given by
C (k ) :≡ f (k) = f 0 (k ), which comes equipped with a base point
p  ( p 0 ) −1 : C (0 ),
and the family of equivalences
λ(α : f (k) = f 0 (k )). ( H (k )  apek (α))  H 0 (k )−1 : ∏ (k:Z) C (k ) ' C (succ(k )).
110 CHAPTER III. UNIVALENT MATHEMATICS

One way of phrasing the following corollary, is that Z is the ‘initial type equipped
with a point and an automorphism’.

Corollary 15.4.4. For any type X equipped with a base point x0 : X and an automorphism
e : X ' X, the type

∑( f :Z→X ) ( f (0) = x0 ) × (( f ◦ succ) ∼ (e ◦ f ))

is contractible.

15.5 The identity type of the circle

Lemma 15.5.1. The total space ∑(t:S1 ) E (t) of the fundamental cover of S1 is contractible.

Proof. By Corollary 15.3.3 it suffices to construct a function

h : ∏ (k:Z) (base, 0E ) = (base, k E )

equipped with a homotopy

H : ∏ (k:Z) h(succ(k )E ) = h(k )  segment-helix(k ).

We obtain h and H by the elimination principle of Lemma 15.4.1. Indeed, the family P
over the integers given by P(k ) :≡ (base, 0E ) = (base, k E ) comes equipped with a term
refl(base,0E ) : P(0), and a family of equivalences

∏ (k:Z) P(k ) ' P(succ(k ))

given by k, p 7→ p  segment-helix(k ).

Theorem 15.5.2. The family of maps

∏ (t:S1 ) (base = t) → E (t)

sending reflbase to 0E is a family of equivalences. In particular, the loop space of the circle is
equivalent to Z.

Proof. This is a direct corollary of Lemma 15.5.1 and Theorem 9.2.2.

Corollary 15.5.3. The circle is a 1-type and not a 0-type.

Proof. To see that the circle is a 1-type we have to show that s = t is a 0-type for
every s, t : S1 . By Exercise 14.1 it suffices to show that the loop space of the circle is
a 0-type. This is indeed the case, because Z is a 0-type, and we have an equivalence
(base = base) ' Z.
Furthermore, since Z is a 0-type and not a (−1)-type, it follows that the circle is a
1-type and not a 0-type.
15. EXERCISES 111

Exercises
15.1 Show that the map
Z → Ω ( S1 )
is a group homomorphism. Conclude that the loop space Ω (S1 ) as a group is
isomorphic to Z.
15.2 Use the fundamental cover of the circle to show that
 
¬ ∏ (t:S1 ) base = t .

15.3 (a) Show that for every x : X, we have an equivalence

 
∑( f :S1 →X ) f (base) = x ' ( x = x )

(b) Show that for every t : S1 , we have an equivalence

 
∑( f :S1 →S1 ) f (base) = t ' Z

The base point preserving map f : S1 → S1 corresponding to k : Z is called

the degree k map on the circle, and is denoted by deg(k ).
(c) Show that for every t : S1 , we have an equivalence
 
∑(e:S1 'S1 ) e(base) = t ' 2

15.4 The (twisted) double cover of the circle is defined as the type family T :≡
D(2, neg) : S1 → U , where neg : 2 ' 2 is the negation equivalence of Exercise 7.5.
(a) Show that ¬(∏ (t:S1 ) T (t)).
(b) Construct an equivalence e : S1 ' ∑(t:S1 ) T (t) for which the triangle
e
S1 ∑(t:S1 ) T (t)

deg(2) pr1

S1

commutes.
15.5 Show that (S1 ' S1 ) ' S1 + S1 . Conclude that a univalent universe containing a
circle is not a 1-type.
15.6 (a) Construct a family of equivalences
∏ (t:S1 ) (t = t) ' Z .

(b) Use Exercise 14.5 to show that (idS1 ∼ idS1 ) ' Z.

(c) Use Exercise 11.7 to show that
has-inverse(idS1 ) ' Z,
and conclude that has-inverse(idS1 ) 6' is-equiv(idS1 ).
15.7 Consider a map i : A → S1 , and assume that i has a retraction. Construct a term of
type
is-contr( A) + is-equiv(i ).
Bibliography

[1] Erret Bishop. Foundations of constructive analysis. New York: McGraw-Hill Book Co.,
1967, pp. xiii+370.
[2] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations
of Mathematics. Institute for Advanced Study: [Link]
book, 2013.

113
Index

( –, – ), 23 anti-symmetric
−1Z , 21 poset, 86
∅, see empty type ap f , see action on paths
02 , 20 ap-comp, 30
02 6= 12 , 47 ap-concat, 31
0N , 14 ap-id, 30
0Z , 21 ap-inv, 31
1, see unit type ap-refl, 31
12 , 20 apd f , 32
1Z , 21 associativity
2, see booleans of addition on N, 32
3-for-2 property of addition on Z, 48
of contractible types, 56 of dependent function composition,
of equivalences, 47 12
of function composition, 11
A + B, see coproduct of multiplication on N, 32
a = x, see identity type of path concatenation, 29
A → B, see function type of Σ-types, 47
A ' B, see equivalence Aut, 90
as relation, 87 automorphism group, 90
truncatedness, 86 axiom
A × B, see cartesian product function extensionality, 74
action on generators univalence, 83
for the circle, 99 axiom K, 68
action on paths, 30–31
ap-comp, 30 B A , see function type
ap-concat, 31 base, 96
ap-id, 30 base case, 15
ap-inv, 31 β-rule
ap-refl, 31 for Π-types, 9
addN , 16 bi-implication, 81, 85
addN (m) is an embedding, 71 bi-invertible map, see equivalence
addZ , 24 binomial coefficient, 18, 77
addition on N, 16–17 binomial theorem, 76
annihilation laws Bishop on the positive integers, 13
cartesian product, 46 boolean algebra, 20, 24
anti-reflexive, 40 boolean logic, 20

115
116 INDEX

boolean operations, 20 fundamental cover, 104–111

booleans, 20 total space is contractible, 110
02 , 20 is a 1-type, 110
12 , 20 loop, 96
computation rules, 20 classical-Prop
conjunction, 20 classical-Prop ' 2, 87
constb is not an equivalence, 47 closed term, 2
disjunction, 20 closed type, 2
exclusive disjunction, 24 coherently invertible, 79
if and only if, 24 is a proposition, 81
implication, 24 coherently invertible map, 53
induction principle, 20 is a contractible map, 53
neg2 , 20 commutativity
negation, 20 of addition on N, 32
Peirce’s arrow, 24 of addition on Z, 48
rules, 24 of coproducts, 47
Sheffer stroke, 24 of multiplication on N, 32
comp( g, f ), 10
cartesian product, 23–24 composition
annihilation laws, 46 of dependent functions, 12
computation rule, 24 associativity, 12
ind× , 24 unit laws, 13
induction principle, 24 of equivalences, 47
rules, 24 of functions, 10
universal property, 78 associativity, 11
category, 94 unit laws, 11
of groups, 94 of group homomorphisms, 91
of posets, 95 of morphisms, 94
of semi-groups, 94 of semi-group homomorphisms, 90
of sets, 94 computation rules
poset, 94 for N, 16
category laws, 94 of booleans, 20
for functions, 11 of cartesian product, 24
center of contraction, 50 of coproduct, 21
change of variables, 6 of Σ-types, 23
characterization of identity type of the circle, 96
contractible type, 56 of unit type, 19
coproduct, 62–64 of Z, 22
fiber, 52 con-inv, 32
fundamental theorem of identity types, concat, 28
57–66 is a family of equivalences, 46
Σ-type, 44–46 is an embedding, 95
choice, 75 concat0 , 46
choice−1 , 75 is a family of equivalences, 46
circle, 95–111 concat-list, 25
base, 96 concatenation
INDEX 117

for identifications, 28 dependent function

of lists, 25 dependent action on paths, 32
cons( a, l ), 25 dependent function type, 7–13
constx , 12 β-rule, 9
constant family, 5 change of bound variable, 8
constant function, 12 computation rules, see β- and η-rules
context, 1–3 conversion rule, 8
empty context, 2 elimination rule, see evaluation
contractible η-rule, 9
retract of, 74 evaluation, 9
weak function extensionality, 74 formation rule, 8
contractible map, 52–56 introduction rule, see λ-abstraction
is an equivalence, 52 λ-abstraction, 9
contractible type, 49–57 λ-conversion, 9
3-for-2 property, 56 dependent pair, 23
center of contraction, 50 dependent pair type, 23
closed under cartesian product, 56 ( –, – ), 23
closed under retracts, 56 computation rule, 23
contraction, 50 EqΣ , 45
identity types of, 56 identity type, 44–46
is a proposition, 66 indΣ , 23
is equivalent to 1, 56 induction principle, 23
contraction, 50 left unit law, 56
conversion rule pr1 , 23
term, 7 pr2 , 23
variable, 3 rules, 24
coproduct, 21–22 dependent type theory, 1–7
computation rules, 21 dependent universal property
disjointness, 62–64 of the circle, 97
functorial action, 48 derivation, 5–6
identity type, 62–64 descS1 , 104
ind+ , 21 descent data
induction principle, 21 for the circle, 104
inl, 21 dgenS1 , 96
inr, 21 disjoint sum, see coproduct
is commutative, 47 disjointness of coproducts, 62–64
rules, 24 distributivity
unit laws, 46 of inv over concat, 32
universal property, 81 of mulN over addN , 32
Z, 21 of Π over Σ, 75

d|n ES1 , 105

is a proposition if d > 0, 71 embedding, 61–62
dependent action on generators closed under homotopies, 64
for the circle, 96 empty context, 2
dependent action on paths, 32, 96 empty type, 19
118 INDEX

ind∅ , 19 family, 3
induction principle, 19 constant family, 5
is a proposition, 66 fiber of, 4
rules, 24 fibers of projection map, 56
universal property, 81 of finite types, 38
encoding of a type in a universe, 33 transport, 31
enough universes, 35–37 trivial family, 5
Eq2 , 40 universal family, 34
Eq-fib, 52 family of equivalences, 57–60
EqN , 38 fib f (b), 52
EqΣ , 45 fiber, 52
eq-equiv, 83 characterization of identity type, 52
eq-htpy, 73 Eq-fib, 52
eq-pair, 45 of a family, 4
equiv-eq, 83 of tot ( f ), 57
is a group isomorphism, 95 Fibonacci sequence, 14, 18, 25
equivalence, 41–49 fibrant replacement, 57
3-for-2 property, 47 Fin, 76
closed under homotopies, 46 Fin, 38
composition, 47 finite types, 38
has an inverse, 43 first projection map, 23
inverse, 43 flatten-list, 25
is a contractible map, 56 fold-list, 25
is an embedding, 62 function
pointed equivalence, 87 action on paths, 30
postcomposition, 80 addition on N, 16–17
precomposition, 78 binomial coefficient, 18
equivalence induction, 84 const, 12
equivalence relation constant function, 12
observational equality on N, 40 exponentiation on N, 18
η-rule, 85 factorial operation, 18
for Π-types, 9 has a retraction, 43
ev-inl-inr, 81 has a section, 43
ev-pair, 77, 78 has an inverse, 43
ev-pt, 50, 81 is an equivalence, 43
ev-refl, 78 maxN , 18
evaluation, 9 minN , 18
exponentiation function on N, 18 mulN , 18
extensionality principle pr1 , 23
for functions, 73 pr2 , 23
for propositions, 85 predZ , 24
for types, 83 succN , 14
succZ , 22
f + g, see functorial action, of coproducts swap, 13
f ∼ g, see homotopy is an equivalence, 44
factorial operation, 18 function extensionality, 73
INDEX 119

function type, 1, 10 has-inverse(id ) ' (id ∼ id ), 81

composition, 10 helix, 105
identity function, 10 higher inductive type
functorial action circle, 96
of coproducts, 48 hom( G, H ) for groups, 91
fundamental cover hom( G, H ) for semi-groups, 90
of the circle, 104–111 homomorphism
fundamental theorem of identity types, of groups, 91
44, 57–66, 73, 83, 92 homotopy, 41–42
formulation with retractions, 65 commutative diagram, 42
formulation with sections, 65 groupoid laws, 41–42
htpy-concat, 41
g ◦ f , 10
htpy-inv, 41
Γ ` a : A, 2
htpy-nat, 54
Γ ` a ≡ b : A, 2
htpy-refl, 41
Γ ` A ≡ B type, 2
iterated, 41
Γ ` A type, 2
naturality, 54
genS1 , 99
whiskering operations, 42
Goldbach’s Conjecture, 32
homotopy fiber, see fiber
graph
homotopy induction, 73
of a function, 87
Homotopy interpretation, 26
Group, 89
horizontal line, see inference rule
identity type, 93
htpy-concat, 41
is a 1-type, 93
is a family of equivalences, 80
is a category, 94
htpy-concat0
group, 34, 89
is a family of equivalences, 80
automorphism group of set, 90
htpy-eq, 73
homomorphism, 91
is an equivalence, 73
is a category, 94
loop space of 1-type, 89 htpy-inv, 41
Sn , 90 is an equivalence, 80
Z, 90 htpy-nat, 54
group homomorphism htpy-refl, 41
isomorphism, 91 hypothetical term, 2
preserves units and inverses, 95
Id A , see identity type
group operations
on Z, 24 id A , 10
groupoid laws identification, 27
of homotopies, 41–42 identification elimination, 27
of identifications, 28–30 identity function, 5, 10
is an equivalence, 44
H · f , see homotopy, whiskering opera- identity homomorphism
tions for groups, 91
h · H, see homotopy, whiskering opera- of semi-groups, 90
tions identity morphism, 94
has an inverse, 43 identity system, 60–61
has-inverse( f ), 43 identity type, 2, 26–33
120 INDEX

action on paths, 30–31 of coproduct, 21

con-inv, 32 of empty type, 19
coproduct, 62–64 for N, 14
distributive-inv-concat, 32 of Σ-types, 23
identification, 27 of the circle, 96
identification elimination, 27 of the identity type, 27
induction principle, 27 of unit type, 19
inv-con, 32 of Z, 21
lift, 32 path induction, 27
Mac Lane pentagon, 33 singleton induction, 50
of a fiber, 52 inductive step, 15
of a Π-type, 73 inductive type, 13–33
of a Σ-type, 44–46 booleans, 20
of a universe, 83 cartesian product, 23–24
of contractible type, 56 circle, 95–111
of Group, 93 coproduct, 21–22
of retract is retract, 47 dependent pair type, 23
of Semi-Group, 92 empty type, 19
of U∗ , 87 identity type, 26–33
path, 27 list( A), 25
path induction, 27 natural numbers, 14
path-ind, 27 unit type, 18–19
refl, 27 inference rule, see rule
rules, 27 conclusion, 1
total space is contractible, 51 hypotheses, 1
tower of identity types, 30 injective function, 69
transport, 31 inl, 21
universal property, 78 is an embedding, 64
iff-eq, 85 inr, 21
ind+ , 21 is an embedding, 64
ind∅ , 19 integers, 21–22, 24–25
ind1 , 19 −1Z , 21
ind2 , 20 0Z , 21
indN , 15 1Z , 21
indΣ , 23 addZ , 24
ind× , 24 computation rules, 22
indexed term, 3 Fibonacci sequence, 25
indexed type, 3 group laws, 48
induction principle in-neg, 21
for equivalences, 84 in-pos, 21
for homotopies, 73 induction principle, 21
for N, 16 mulZ , 24
identification elimination, 27 negZ , 24
list( A), 25 predZ , 24
of booleans, 20, 25 succZ , 22
of cartesian products, 24 interchange rule, 6
INDEX 121

inv, 28 htpy-eq, 73
is an equivalence, 46 htpy-inv, 80
inv-con, 32 identity function, 44
inverse inv, 46
of an equivalence, 43 inverse of an equivalence, 43
is an equivalence, 43 neg2 , 47
inverse law operations pair-eq, 45
for identifications, 30 pr1 of contractible family, 56
inverse laws succZ , 47
for a group, 89 swap function, 44
for addition on Z, 48 tot ( f ) of family of equivalences, 58
for semi-group isomorphisms, 91 tr B ( p), 46
inverse operation is contractible
for identifications, 28 factor of contractible cartesian prod-
is a contractible map, 52 uct, 56
equivalence, 56 fiber of an equivalence, 56
is a proposition identity type of contractible type, 56
contractible type, 66 iff singleton induction, 50
d | n for d > 0, 71 is a property, 80
empty type, 66 total space of an identity system, 61
is a set, 68 total space of identity type, 51
natural numbers, 69 total space of opposite identity type,
is an embedding, 62 56
(−1)-truncated map, 71 unit type, 50
∅ → A, 64 is family of equivalences
addN (m), 71 iff tot ( f ) is an equivalence, 58
composite of embeddings, 64 is-coh-invertible( f ), 53
equivalence, 62 is-contr( A), see contractible type
if the action on paths have sections, is a proposition, 80
65 is-contr( f ), see contractible map
injective map into a set, 69 is-decidable
inl (for coproducts), 64 is a proposition, 87
inr (for coproducts), 64 is-emb( f ), 62
left factor of embedding if right fac- is-equiv( f ), 43
tor is an equivalence, 64 is a proposition, 80
mulN (m) for m > 0, 71 is-equiv( f ) ' is-coh-invertible( f ), 81
right factor of embedding if left fac- is-equiv( f ) ' is-contr( f ), 80
tor is an embedding, 64 is-equiv( f ) ' path-split( f ), 81
succN , 71 is-function( R), 87
is an equivalence, 43 is-group, 89
action on paths of an embedding, 62 is a proposition, 89
concat0 (q), 46 is-group0 , 89
concat( p), 46 is a proposition, 89
contractible map, 52 is-iso for semi-groups, 91
htpy-concat0 (K ), 80 is a proposition, 91
htpy-concat( H ), 80 is-prop0 ( A), 66
122 INDEX

is-prop( A), 66 length-list, 25

is-prop( A) ↔ ( A → is-contr( A)), 66 lift, 32
is-prop( A) ↔ is-emb(const? ), 67 list( A), see lists in A
is-prop( A) ↔ is-prop0 ( A), 66 lists in A
is-set( A), 68 concat-list, 25
is-set( A) ↔ axiom-K( A), 68 cons, 25
is-trunck ( A), 69 flatten-list, 25
is-trunck ( A) → is-trunck+1 ( A), 69 fold-list, 25
is-unital, 88 induction principle, 25
is a proposition, 88 length-list, 25
iso( x, y), 94 nil, 25
iso-eq for groups, 93 reverse-list, 25
iso-eq for semi-groups, 92 sum-list, 25
isomorphism, 82 lists in A, 25
in a pre-category, 94 loop, 96
of groups, 91 loop space, 38
of semi-groups of 1-type is a group, 89
preserves unit, 95
is-trunck Mac Lane pentagon, 33
is a proposition, 80 maximum function, 18
iterated homotopies, 41 minimum function, 18
iterated loop space, 38 monoid, 88
morphism, 93
judgment, 1–3 mulN , 18
Γ ` a : A, 2 mulN (m) is an embedding if m > 0,
Γ ` a ≡ b : A, 2 71
Γ ` A ≡ B type, 2 mulZ , 24
Γ ` A type, 2 multiplication
judgmental equality on N, 18
conversion rules, 3
N, see natural numbers
is an equivalence relation, 3
natural numbers, 2, 13–18
of terms, 2
indN , 15
of types, 2
is a closed type, 2
k-truncated map, see truncated map is a poset with divisibility, 86
k-truncated type, see truncated type is a poset with ≤, 86
k-type, 69, 75 is a set, 69
universe of k-types, 86 observational equality, 38
operations on N
λ-abstraction, 9 0N , 14
λ-conversion, 9 addN , 16
laws addition, 16–17
of a category, 94 binomial coefficient, 18
left-inv, 30 exponentiation, 18
left-unit, 29 Fibonacci sequence, 14, 18
left unit law, see unit laws maxN , 18
of Σ-types, 56 minN , 18
INDEX 123

mulN , 18 path constructor, 96

n!, 18 path induction, 27
succN , 14 path-ind, 27
rules for N path-split, 65
computation rules, 16 is a proposition, 81
elimination, see induction path-split( f ), 65
formation, 14 pattern matching, 17
induction, 16 Π-type, see dependent function type
induction principle, 14 pointed equivalence, 87
introduction rules, 14 pointed map, 38
semi-ring laws, 32 pointed type, 37–38
naturality square of homotopies, 54 poset, 86
¬ A, see negation closed under exponentials, 86
neg2 , 20 is a category, 94
is an equivalence, 47 N with divisibility, 86
negZ , 24 N with ≤, 86
negation type of subtypes, 86
of types, 19 pr1 , 23
negation function of contractible family is an equiva-
on booleans, 20 lence, 56
nil, 25 pr2 , 23
pre-category, 93
objects, 93
identity morphism, 94
observational equality
morphisms, 93
EqΣ , 45
objects, 93
of coproducts, 63
of groups, 94
of Π-types, 41
of semi-groups, 94
on 2, 40
of sets, 94
is least reflexive relation, 40
preorder, 94
is reflexive, 40
Rezk complete, 94
on booleans
pre-image, see fiber
02 6= 12 , 47
precomposition map, 78
on N, 38
predZ , 24
is an equivalence relation, 40
predecessor function, 24
is least reflexive relation, 40
is preserved by functions, 40 preorder, 94
Ω, see loop space product of types, 24
Ωn , see iterated loop space program, 8
Rop , 87 projection map
opposite relation, 87 second projection, 23
order relation, 40 projection maps
first projection, 23
pair-eq, 45 proof by contradiction, 19
is an equivalence, 45 proof of negation, 19
pairing function, 23 Prop, 66
partially ordered set, see pset86 is a poset, 86
path, 27 is a set, 85
124 INDEX

property, 68 formation, 14
proposition, 66–68 induction principle, 15
closed under equivalences, 67 introduction rules, 14
propositional extensionality, 85, 86 for type dependency
propositions as types change of variables, 6
conjunction, 24 interchange, 6
ptx , 19 rules for judgmental equality, 3–4
rules for substitution, 4
refl, 27 rules for weakening, 5
reflexive term conversion, 7
poset, 86 variable conversion, 3
reflexive relation, 40 variable rule, 5
relation for unit type, 24
anti-reflexive, 40 identity type, 27
functional, 87
opposite relation, 87 S1 , 96, see circle
order, 40 sec( f ), 43
reflexive, 40 second projection map, 23
retr( f ), 43 section
retract of a map, 43
identity type, 47 section of a family, 3
of a type, 43 Semi-Group, 88
retraction, 43 identity type, 92
reverse-list, 25 is a 1-type, 92
Rezk-complete, 94 is a category, 94
right-inv, 30 semi-group, 88
right-unit, 29 has inverses, 89
right unit law, see unit laws homomorphism, 90
rules is a pre-category, 94
for booleans, 24 unital, 88
for cartesian product, 24 semi-ring laws
for coproduct, 24 for N, 32
for dependent function types set, 34, 68–69
β-rule, 9 isomorphism, 82
change of bound variable, 8 set-level structure, 88
conversion, 8 sets
η-rule, 9 form a category, 94
evaluation, 9 Σ-type, see dependent pair type
formation, 8 associativity of, 47
λ-abstraction, 9 universal property, 77
λ-conversion, 9 sing-comp, 50
for dependent pair type, 24 sing-ind, 50
for empty type, 24 singleton induction, 50
for function types, 10 iff contractible, 50
for N small type, 35
computation rules, 16 Sn , 90
INDEX 125

structure identity principle, 88 truth tables, 20

subset, 67 Twin Prime Conjecture, 32
substitution, 4 type, 2
subtype, 68 closed type, 2
poset, 86 indexed, 3
subuniverse type family, 3
closed under equivalences, 87 type theoretic choice, 75
succN , 14
is an embedding, 71 U ≤k , 86
succZ , 22 U , V , W , see universe
is an equivalence, 47 uniform family, 7
successor function uniform term, 7
on N, 14 unit
on Z, 22 of a unital semi-group, 88
is an equivalence, 47 unit law operations
sum-list, 25 for identifications, 29
swap function, 13 unit laws
is an equivalence, 44 coproduct, 46
symmetric groups, 90 dependent function composition, 12,
13
T , see universal family for a unital semi-group, 88
term, 2 for addition on N, 32
closed term, 2 for addition on Z, 48
indexed, 3 for function composition, 11, 12
term conversion rule, 7 for multiplication on N, 32
tot f ( g), 59 unit type, 18–19
tot ( f ), 57 computation rules, 19
fiber, 57 induction principle, 19
of family of equivalences is an equiv- ind1 , 19
alence, 58 is a closed type, 19
tower of identity types, 30 is contractible, 50
tr B , 31 rules, 24
is a family of equivalences, 46 singleton induction, 50
transitive ?, 19
poset, 86 universal property, 81
transport, 31 unital semi-group, 88
trivial family, 5 has inverses, 89
truncated family of types, 70 univalence axiom, 83, 88
truncated map, 69 families over S1 , 104
truncated type, 66–72 implies function extensionality, 84
closed under embeddings, 70 univalent universe, 83
closed under equivalences, 69 universal family, 33–40
closed under exponentials, 75 universal property
closed under Π, 75 cartesian product, 78
universe of k-types, 86 coproduct, 81
truncation level, 66–72 empty type, 81
126 INDEX

identity type, 78
of the circle, 97
Σ-types, 77
unit type, 81
universe, 33–40
enough universes, 35–37
of contractible types, 86
of k-types, 86
of propositions, 86
of sets, 87
small types, 35
U∗ , 37, 87
identity type, 87

variable, 2
variable conversion rules, 3
variable declaration, 2
variable rule, 5

weak function extensionality, 74, 75, 84

weakening, 3, 5
well-formed term, 2
well-formed type, 2
whiskering operations
of homotopies, 42

Yoneda lemma (type theoretical), 78

Z, see integers
fundamental cover of S1 , 105
is a group, 90