# Homotopy Type Theory

In foundations of mathematics, univalent foundations is an approach to the foundations of constructive mathematics[1] based on the idea that mathematics studies structures on “univalent types” that correspond, under the projection to set-theoretic mathematics, to homotopy types. Univalent foundations are inspired both by the old Platonic ideas of Hermann Grassmann and Georg Cantor and by the “categorical” mathematics in the style of Alexander Grothendieck. It departs from the use of predicate logic as the underlying formal deduction system, replacing it, at the moment, by a version of the Martin-Löf type theory. The development of the univalent foundations is closely related with the development of homotopy type theory.

2017-10-01 Wikipedia [ Univalent foundations ] [ 2017-10-01 https://en.wikipedia.org/wiki/Univalent_foundations ]

this is great, because:

- a new foundation of math, based on constructive proofs. That is, computable.
- links algorithms with math. That is, the how and the what. So that, math can be proved by algorithms more easily.

## Introduction

Homotopy type theory is a new branch of mathematics that combines aspects of several different fields in a surprising way. It is based on a 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. Although the connections between the two are currently the focus of intense investigation, it is increasingly clear that they are just the beginning of a subject that will take more time and more hard work to fully understand. It touches on topics as seemingly distant as the homotopy groups of spheres, the algorithms for type checking, and the definition of weak ∞-groupoids.

Homotopy type theory also brings new ideas into the very foundation of mathematics. On the one hand, there is Voevodsky’s subtle and beautiful univalence axiom. The univalence axiom implies, in particular, that isomorphic structures can be identified, a principle that mathematicians have been happily using on workdays, despite its incompatibility with the “official” doctrines of conventional foundations. On the other hand, we have higher inductive types, which provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory: spheres, cylinders, truncations, localizations, etc. Both ideas are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of “logic of homotopy types”.

This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an “invariant” conception of the objects of mathematics — and convenient machine implementations, which can serve as a practical aid to the working mathematician. This is the Univalent Foundations program. The present book is intended as a first systematic exposition of the basics of univalent foundations, and a collection of examples of this new style of reasoning — but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.

We emphasize that homotopy type theory is a young field, and univalent foundations is very much a work in progress. This book should be regarded as a “snapshot” of just one portion of the field, taken at the time it was written, rather than a polished exposition of a completed edifice. As we will discuss briefly later, there are many aspects of homotopy type theory that are not yet fully understood — and some that are not even touched upon here. The ultimate theory will almost certainly not look exactly like the one described in this book, but it will surely be at least as capable and powerful; we therefore believe that univalent foundations will eventually become a viable alternative to set theory as the “implicit foundation” for the unformalized mathematics done by most mathematicians.