Álvaro Pelayo                                                    











A theory is more impressive the greater the simplicity of its premises, the more kinds of things it relates, and the more extended its area of applicability.

A. Einstein

Click here to go back to Research

Summary of G4 : Homotopy Type Theory

Homotopy type theory is a new field of mathematics which interprets type theory from a homotopical perspective. Voevodsky's univalent foundations program is a research theme based on homotopy type theoretic ideas, and which can be carried out in a computer proof assistant. The goal of Voevodsky's program is developing mathematics in the setting of type theory with an additional axiom which he introduced, the Univalence Axiom. Homotopy type theory is connected to several topics of interest in modern algebraic topology, such as infinity-groupoids and Quillen model structures.

Type theory was invented by Russell (1908), but it was first developed as a rigorous formal system by Church (1930s, 1940s). It now has numerous applications in computer science, especially in the theory of programming languages. In type theory objects are classified using a primitive notion of "type", similar to the data-types used in programming languages. And as in programming languages, these elaborately structured types can be used to express detailed specifications of the objects classified, giving rise to principles of reasoning about them.

In homotopy type theory, one regards the types as spaces, or homotopy types, and the logical constructions as homotopy-invariant constructions on spaces. In this way, one is able to manipulate spaces directly, without first having to develop point-set topology or even define the real numbers.

We hope that in the future, because this development of mathematics can be carried out in a proof assistant such as Coq so that the proofs carry some algorithmic content, it will be possible to extract good algorithms from the proofs.

Some topics I have worked on: