Homotopy type theory : univalent foundations of mathematics / the Univalent Foundations Program, Institute for Advanced Study.

Format:

Book

Contributor:

Awodey, Steve, 1959- organizer.

Coquand, Thierry, 1961- organizer.

Voevodsky, Vladimir, organizer.

Institute for Advanced Study (Princeton, N.J.). Univalent Foundations of Mathematics, host institution.

Language:

English

Subjects (All):

Homotopy theory.

Physical Description:

xiii, 605 pages : illustrations ; 24 cm

Edition:

First edition.

Place of Publication:

[Princeton, New Jersey] : Univalent Foundations Program, Institute for Advanced Study, [2013]

Summary:

"The present work has its origins in our collective attempts to develop a new style of "informal type theory" that can be read and understood by a human being, as a complement to a formal proof that can be checked by a machine. Univalent foundations is closely tied to the idea of a foundation of mathematics that can be implemented in a computer proof assistant."--Page vi.

"Homotopy type theory is a new branch of mathematics that combines aspects of several different fields in a surprising way. It is based on the recently discovered connection between homotopy theory and type theory. Homotopy theory is an outgrowth of algebraic topology and homological algebra, with relationships to higher category theory; while type theory is a branch of mathematical logic and theoretical computer science."--Introduction.

Notes:

Book version: first-edition-1277-g3274cb3.

"A special year on Univalent Foundations of Mathematics was held in 2012-13 at the Institute for Advanced Study, School of Mathematics, organized by Steve Awodey, Thierry Coquand, and Vladimir Voevodsky."--Page v.

Includes bibliographical references (pages 567-577) and indexes.

OCLC:

976446196