Homotopical inductive types

Over the past few years, new surprising connections have emerged between two traditionally distant areas of mathematics: mathematical logic (which is generally concerned with the study of the forms of reasoning used in mathematics) and homotopy theory (which is interested in understanding and classifying various notions of space). These connections are useful because they provide a clear
geometric intuition that helps us to work with a class of logical systems, known as type theories. On that basis, the Fields medallist Vladimir Voevodsky has formulated an ambitious research programme, called the Univalent Foundations of Mathematics programme, that seeks to develop a new foundations of mathematics on the basis of type theories that include new axioms motivated by homotopy theory.

The proposed research seeks to advance our understanding of the type theories proposed by Voevodsky in order to develop the Univalent Foundations programme. Our first goal is to understand better the relationship between the type theories introduced by Voevodsky and axiomatic set theories, which represent the more traditional approach to foundations of mathematics. In particular, we want to clarify the logical status of the Univalence Axiom, a new axiom which allows us to treat objects that share all structural properties as equal. Furthermore, we wish to gain further insight into a variation, again motivated by homotopy theory, over the standard way of defining types.

The modern world relies in an essential way on computer systems to run important tasks in a variety of areas: from finance and medicine to transport and energy. When computer systems are used in safety-critical applications (such as controlling the functioning of a nuclear power station or coordinating the signal system of a train network), it is essential that their correctness is established without doubt, and not merely indicated by tests.

One successful approach to the verification of software correctness has been to develop integrated software systems, known as proof assistants, in which it is possible to write computer programs, specify requirements, and formally prove that these requirements hold. Thus, these systems give us a way of creating correct-by-construction programs, which is beneficial also in economic terms since it eliminates the difficult process of debugging. The development of proof assistants involved a combination of ideas of mathematical logic and computer science, in a way that is reminiscent of the very origin of computer programming. Indeed, proof assistants are also used in the formalisation of mathematical proofs, so as to guarantee their correctness.

The proposed research focuses on logical systems, known as type theories, which are at the core of some of the most powerful proof assistants (such as the Coq system). In particular, we seek to advance our understanding of a new class of type theories which have been recently formulated by the Fields medallist Vladimir Voevodsky, thanks to the discovery of surprising connections between
mathematical logic and homotopy theory (an area of mathematics that studies general notions of space).

Our proposed research will benefit directly the academic communities working in mathematical logic, homotopy theory and higher-dimensional category theory by improving our understanding of this new class of type theories and of the connections between these subjects. Our work is likely to impact also the ongoing design of new proof assistants based on these new type theories, since it aims to obtain precise information on their expressive power. These new proof assistants, in turn, will benefit society in general by facilitating the creation of correct-by-construction computer programs.