Introduction to homotopy type theory / Egbert Rijke.

Format:

Book

Author/Creator:

Rijke, Egbert, author.

Series:

Cambridge studies in advanced mathematics ; 219.

Cambridge studies in advanced mathematics ; 219

Language:

English

Subjects (All):

Homotopy theory.

Physical Description:

1 online resource

Place of Publication:

Cambridge : Cambridge University Press, 2026.

Summary:

"This up-to-date introduction to type theory and homotopy type theory will be essential reading for advanced undergraduate and graduate students interested in the foundations and formalization of mathematics. The book begins with a thorough and self-contained introduction to dependent type theory. No prior knowledge of type theory is required. The second part gradually introduces the key concepts of homotopy type theory: equivalences, the fundamental theorem of identity types, truncation levels, and the univalence axiom. This prepares the reader to study a variety of subjects from a univalent point of view, including sets, groups, combinatorics, and well-founded trees. The final part introduces the idea of higher inductive type by discussing the circle and its universal cover. Each part is structured into bite-size chapters, each the length of a lecture, and over 200 exercises provide ample practice material"-- Cambridge University Press.

Contents:

Dependent type theory

Dependent function types

The natural numbers

More inductive types

Identity types

Universes

Modular arithmetic via the Curry-Howard interpretation

Decidability in elementary number theory

Equivalences

Contractible types and contractible maps

The fundamental theorem of identity types

Propositions, sets, and the higher truncation levels

Function extensionality

Propositional truncations

Image factorizations

Finite types

The univalence axiom

Set quotients

Groups in univalent mathematics

General inductive types

The circle

The universal cover of the circle.

Notes:

Includes bibliographical references and index.

Online resource; title from PDF title page (Cambridge University Press, viewed November 13, 2025).

Other Format:

Print version: Rijke, Egbert. Introduction to homotopy type theory

ISBN:

9781108933568

1108933564

OCLC:

1529915730

Publisher Number:

CIPO000255134

Access Restriction:

Restricted for use by site license