# nLab Introduction to Homotopy Type Theory

### Context

#### Homotopy theory

This entry collects links related to the forthcoming book

• Introduction to Homotopy Type Theory

Cambridge University Press

arXiv:2212.11082 (359 pages)

which introduces homotopy type theory in general and in particular Martin-Löf's dependent type theory, the Univalent Foundations for Mathematics and synthetic homotopy theory.

The book is based on a course taught by the author at Carnegie Mellon University in the spring semester of 2018:

The original writeup of these course notes

contains considerably more material than retained in the above arXiv version.

Other versions:

## Contents

Chapter I introduces the reader to Martin-Löf's dependent type theory. The fundamental concepts of type theory are explained without immediately jumping into the homotopy interpretation of type theory.

$\;\;\;1.$ Dependent Type Theory

$\;\;\;2.$ Dependent function types

$\;\;\;3.$ The natural numbers

$\;\;\;4.$ More inductive types

$\;\;\;5.$ Identity types

$\;\;\;6.$ Universes

$\;\;\;7.$ Modular arithmetic via the Curry-Howard isomorphism

$\;\;\;8.$ Decidability in elementary number theory

Chapter II is an exposition of the Univalent Foundations for Mathematics. This chapter gradually extends dependent type theory with function extensionality, propositional truncation, the univalence axiom, and the type theoretic replacement axiom.

$\;\;\;9.$ Equivalences

$\;\;\;10.$ Contractible types

$\;\;\;11.$ The fundamental theorem of identity types

$\;\;\;12.$ Propositions, sets, and the higher truncation levels

$\;\;\;13.$ Function extensionality

$\;\;\;14.$ Propositional truncations

$\;\;\;15.$ Image factorizations

$\;\;\;16.$ Finite types

$\;\;\;17.$ The univalence axiom

$\;\;\;18.$ Set quotients

$\;\;\;19.$ Groups in univalent mathematics

$\;\;\;20.$ General inductive types

Chapter III studies the circle as a higher inductive type.

$\;\;\;21.$ The circle

$\;\;\;22.$ The universal cover of the circle

An older version of the book ended:

$\;\;\;22.$ Homotopy pullbacks

$\;\;\;23.$ Homotopy pushouts

$\;\;\;24.$ Cubical diagrams

$\;\;\;25.$ Universality and descent for pushouts

$\;\;\;26.$ Sequential colimits

$\;\;\;27.$ Homotopy groups of types

$\;\;\;28.$ The classifying type of a group

$\;\;\;29.$ The Hopf fibration

$\;\;\;30.$ The real projective spaces

$\;\;\;31.$ Truncations

$\;\;\;32.$ Connected types and maps

$\;\;\;33.$ The Blakers-Massey theorem

$\;\;\;34.$ Higher group theory

## Formalization

category: reference

Last revised on January 3, 2023 at 22:58:15. See the history of this page for a list of all contributions to it.