Á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

 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:

• Univalent Study of Basic p-adic Structures:

one of my motivations for the construction of the aforementioned algorithms is to help solve some problems concerning operator theory and integrable systems which are of particular interest in applications. For instance, one outstanding problem is: given numerical spectral data about a p-adic quantum system (coming from an experiment), extract an algorithm to reconstruct the classical integrable system (this is connected to groups G1 and G2).Voevodsky, myself, and Warren have taken first steps in this direction by giving a homotopy type theoretic construction of the p-adic numbers in the setting of Voevodsky's univalent foundations (we also implemented the construction in the Coq proof assistant). The construction involves a univalent description of basic results in number theory and group theory;

• First Steps in Univalent p-adic Systems:

a p-adic symplectic form may be defined as in the real case. The closedness condition makes sense in the p-adic setting, and so does the non-degeneracy condition (in fact, over any field). In the real setting, a theorem of Darboux says that all symplectic forms are locally equivalent, so real symplectic manifolds have no local invariants. It is natural to wonder whether this result holds in the p-adic setting "as is". One should restrict to the analytic setting since the closedness condition is a system of differential equations. We are working on the symplectic p-adic setting further, with an eye towards the development and univalent implementation of a theory of p-adic integrable systems;

• Revisiting the Basic Literature on Homotopy Type Theory:

Awodey, myself, and Warren have worked on explaining in non-specialized, non-technical, terms some of the basic literature on homotopy type theory and Voevodsky's univalent foundations program (which requires knowledge of homotopy theory and mathematical logic) making en emphasis on the connections to other branches of mathematics and theoretical computer science