Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory

Over the past few years it has become apparent that there is a surprising and deep connection between constructive logic and higherdimensional structures in algebraic topology and category theory, in the form of an interpretation of the dependent type theory of Per Martin-Löf into classical homotopy theory. The interpretation results in a bridge between the worlds of constructive and classical mathematics which promises to shed new light on both. This mini-workshop brought together researchers in logic, topology, and cognate fields in order to explore both theoretical and practical ramifications of this discovery. Mathematics Subject Classification (2000): 03B15, 55Pxx. Introduction by the Organisers The mini-workshop The Homotopy Interpretation of Constructive Type Theory, organised by Steve Awodey (Pittsburgh), Richard Garner (Sydney), Per MartinLöf (Stockholm) and Vladimir Voevodsky (Princeton) was held between February 27th and March 5th 2011. It brought together researchers from three different continents and a number of different fields; some known for their work in constructive mathematics and categorical logic, others for their work in higher-dimensional category theory, and others still for their work in algebraic topology and homotopy theory. What brought this seemingly disparate group of individuals together was a desire to understand more completely a connection recently established between these three areas: one mediated by the dependent type theory of Per Martin-Löf. 2 Oberwolfach Report 11/2011 Martin-Löf developed his dependent type theory in the 1970’s to provide a rigourous constructive foundation for mathematics. Besides its philosophical and theoretical interest, constructive type theory is of increasing practical importance, since its constructivity is also a kind of computability: thus it can be viewed as a particularly sophisticated kind of programming language, and in this guise, it provides the foundation for a number of computerised “proof assistants”—such as Epigram, Agda and Coq—which permit the large-scale formalisation and verification of parts of mathematics and computer science. As with any logical system, it is meaningful to ask what an appropriate notion of model might be for dependent type theory. It is in considering this question that the connection with homotopy theory and higher category theory is manifested. Since the 1980’s we have had a notion of categorical model for dependent type theory: this being a category equipped with certain extra structure suitable for modelling the entities present in the logic. But what has only been realised over the past five or so years is that the extra categorical structure required to model the notion of equality in dependent type theory corresponds in a very precise manner to the structure of a weak factorisation system such as occurs in Quillen’s theory of abstract homotopical algebra, and which is of importance in the study of higher-dimensional category theory. This basic insight suggests that further, precise, links might be made between the three areas mentioned above, and a small but growing body of work has begun to show that this is the case. The purpose of this workshop was to bring together researchers active in these areas—and interested in their intersection—in order to take stock of the current situation and to determine in which further directions these ideas might fruitfully be pushed. A particular goal of the workshop was to provide a forum for Vladimir Voevodsky—who has been considering questions in this area since 2006, but working broadly independently of other involved researchers—to communicate at length his own ideas about, and visions for, the topic at hand. In line with this latter objective, approximately half of the itinerary for the workshop was given over to a series of lectures by Voevodsky. In these, he described his programme of “univalent foundations”; its objective being to exploit the connection between dependent type theory and homotopy theory to provide a foundation for mathematics, based on dependent type theory, which is intrinsically homotopical—in the sense of having as its basic entities not only sets, but the entire taxonomy of homotopy types. This foundational endeavour is not merely of theoretical interest; for as described above, Martin-Löf’s type theory underpins a number of computer-based proof assistants, and an important part of the univalent-foundational project is that its toolset should include a workable computer system in which modern mathematics, including its homotopy-theoretic and higher-dimensional aspects, may be formalised. These two sides of the project— the theoretical and the practical—were reflected in two streams to Voevodsky’s lectures. The first dealt with the practical issues surrounding the development of Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory 3 mathematics within these foundations, aided by the proof-assistant Coq. The second was devoted to showing the consistency of the univalent foundations relative to classical mathematics; it did so by exhibiting a model for these foundations—which are an extension of Martin-Löf’s dependent type theory by a homotopy-theoretic reflection principle called the “univalence axiom”—in the algebraic topologist’s category of simplicial sets. The remaining half of the workshop’s itinerary was filled by talks from its other participants. Given the rather diverse backgrounds of the audience, it was thought prudent to devote the first two days of these talks to expository surveys which, taken together, would ensure that everyone present was fully equipped to process the material that was being presented to them. The remainder of the talks described some of the most recent developments in the area, both in relation to Voevodsky’s univalent foundations, and otherwise. The programme was rounded out by an open problems session which helped to crystallise those questions around which future research might accrete. The organisers would like to advance their thanks, on behalf of all the workshop participants, to Mathematisches Forschungsinstitut Oberwolfach for their efficient and unobtrusive arrangement of the practical aspects of this workshop, and for providing a quietly inspiring backdrop to a most scientifically fruitful meeting. Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory 5 Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory