Homotopy Type Theory - Logic and Its Applications - page 1

Homotopy Type Theory

Steve Awodey

Carnegie Mellon University
[e-mail]

Abstract. Homotopy Type Theory is a new, homotopical interpretation
of constructive type theory. It forms the basis of the recently proposed
Univalent Foundations of Mathematics program. Combined with a com-
putational proof assistant, and including a new foundational axiom - the
Univalence Axiom - this program has the potential to shift the theoret-
ical foundations of mathematics and computer science, and to affect the
practice of working scientists. This talk will survey the field and report
on some of the recent developments.

Overview

- Homotopy Type Theory is a recently discovered connection between Logic
and Topology.
- It is based on an interpretation of intensional Martin-Lof type theory into
homotopy theory.
- Univalent Foundations is an ambitious new program of foundations of math-
ematics based on HoTT.
- New constructions based on homotopical intuitions are added as Higher In-
ductive Types, providing classical spaces, (higher) quotients, truncations,
etc.
- The new Univalence Axiom is also added. It implies that isomorphic struc-
tures are equal, in a certain sense.
- And a new “synthetic” style of axiomatics is used, simplifying and shortening
many proofs.
- A large amount of classical mathematics has been developed in this new
system: basic homotopy theory, higher category theory, real analysis, com-
mutative algebra, cumulative hierarchy of set theory, ....
- Proofs are formalized and verified in computerized proof assistants (e.g.
Coq).
- There is a comprehensive topic containing the informal development.

Type Theory

Martin-Lof constructive type theory consists of:

-Types: X,Y,...,A × B, A → B,...