From June 2 to June 6, at Institut Henri Poincaré.
Semantics of type theory has been a driving force for its development since the 1980s. It has been based on more traditional semantics for systems for constructive mathematics like realizability and topological interpretations, or in terms of categorical logic.
A typical example is Homotopy Type Theory (HoTT) which has been inspired by the groupoid model and subsequent models based on abstract homotopy theory. Currently, there is a ongoing effort to understand in which way HoTT can be understood as the internal language of infinity toposes (“sheaves of spaces”) as developed by Joyal, Lurie and Rezk. Another open question is to which extent these model constructions can be performed in type theory itself with the aim of providing Voevodsky's Univalence Axiom with a computational meaning.
Many of the talks will center around these questions. Others will concentrate on relations to constructive mathematics in a more traditional sense and the semantics of programming languages.
We plan to provide enough time for discussion and joint work on questions triggered by the invited talks.
|Monday 2 June|
|10h30-12h00||Per Martin-Löf||Sample space-time|
|14h00-15h30||Peter Dybjer||What is a model of intuitionistic type theory|
|16h00-17h30||Steve Awodey||Natural Models of Type Theory|
|Tuesday 3 June|
|10h30-12h00||André Joyal||Categorical homotopical logic|
|14h00-15h30||Erik Palmgren||Models of dependent types and dependently typed logic and their formalization in type theory|
|Wednesday 4 June|
|10h30-12h00||Guillaume Munch-Maccagnoni||Polarities and classical constructiveness|
|14h00-15h30||Joachim Kock||Univalence in locally cartesian closed infinity-category|
|16h00-17h30||Martin Hofmann||Revisiting the categorical interpretation of type theory|
|Thursday 5 June|
|10h30-12h00||Denis-Charles Cisinski||Univalence for elegant models of homotopy types|
|14h00-15h30||Ronnie Brown||Intuitions for cubical models of homotopy types|
|16h00-17h30||Simon Huber||A Model of Type Theory in Cubical Sets|
|Friday 6 June|
|10h30-12h00||Andrej Bauer||Constructive Model Categories|
|14h00-15h30||Vladimir Voevodsky||B-systems - a link which connects the syntax of dependent type theories with their semantics|
Natural models of type theory
One thing missing from homotopy type theory is a notion of model that is both faithful to the precise formalism of type theory and yet general and flexible enough to be a practical tool. Past attempts have relied either on highly structured categories corresponding closely to the syntax of type theory, such as the categories with families of Dybjer, or more natural and flexible categorical models based on homotopical algebra. The former are, however, somewhat impractical to work with semantically, while the latter must be equipped with unnatural and non-trivial coherence conditions. We present a new approach which combines these two strategies while retaining some of the advantages of each. It is based on the observation that a category with families is the same thing as a representable natural transformation, in the sense of Grothendieck. Ideas from Voevodsky and Lumsdaine-Warren are also used.
Constructive Model Categories
In this talk I will discuss the issues which arise when one wants to construct a model category based on the traditional notion of paths as continuous maps from the interval, in a constructive framework such as Bishop constructive mathematics or extensional type theory. Such models would actually embody the intuitive idea that identity types are paths in a space, while preserving computability, and would also give us a plethora of examples via interpretations in models of constructive mathematics.
Intuitions for cubical methods in nonabelian algebraic topology
The talk will start from the 1-dimensional Seifert-van-Kampen Theorem for the fundamental group, then groupoid, and so to a use of certain strict multiple groupoids for higher versions. These allow for some precise nonabelian calculations of homotopy types, obtained by a gluing process. Cubical methods are important because of the ease of writing multiple compositions, leading to “algebraic inverses to subdivision”, relevant to higher dimensional local-to-global problems. Also the proofs involve some ideas of 2-dimensional formulae and rewriting. The use of *strict* multiple groupoids is essential to obtain homotopy type descriptions as *colimits* and hence precise calculations.
Another idea is to use both a “broad” and a “narrow” model of a particular kind of homotopy types, where the broad model is used for conjectures and proofs, while the narrow model is used for calculations and relation to classical methods. The algebraic proof of the equivalence of the two models then gives a powerful tool, for example for transferring monoidal closed structures from a cubical model.
Univalence for elegant models of homotopy types
What is a model of intuitionistic type theory?
I will discuss different notions of model Martin-Löf's intuitionistic type theory. I will take an intuitionistic perspective follwing Martin-Loef's seminal paper “About models for intuitionistic type theories and the notion of definitional equality” from 1975 and mention both foundational and mathematical aspects. Both game semantic and category theoretic considerations are illuminating and I shall discuss their role.
Revisiting the categorical interpretation of type theory
A Model of Type Theory in Cubical Sets
We present a model of Martin-Löf type theory in a constructive meta-theory. This model is based on a variant of cubical sets and can be seen of a constructive version of Voevodsky's model based on Kan simplicial sets.
Categorical homotopical logic
Many aspects of homotopy (type) theory are best described in the language of category theory. What is an elementary infinity topos?
Univalence in locally cartesian closed infinity-categories
I'll explain the meaning of univalence in the setting of presentable locally cartesian closed infinity-categories. Univalent families correspond precisely to bounded local classes of maps in the sense of Lurie. Lurie shows that locality of the class of all maps is equivalent to the infinity-topos axiom. To exhibit large univalent families outside the realm of toposes, we introduce notions of infinity-quasitoposes, as certain infinity-categories of separated presheaves, sitting in between two infinity-toposes, and show that the map classifier in the small topos induces a univalent family in the quasi-topos. This is joint work with David Gepner.
Polarities and classical constructiveness
I will recall what constructive can mean in the context of classical logic, as accounted for by double negation translations and control operators in programming. Girard proposed a few years back a classical sequent calculus where negation is strictly involutive (¬¬A = A) by taking formally into account the polarity of connectives. I will show that this idea is very natural from the point of view of control operators, leading us to a natural deduction where negation is involutive (¬¬A ≅ A). One of the main aspect is that we do not consider that composition needs to be associative when the middle map is from positives to negatives. In a second time I will therefore introduce duploids, which characterises this non-associative composition directly, and relate them to adjunctions.
Models of dependent types and dependently typed logic and their formalization in type theory
The modeling of type theory in type theory itself is a difficult problem due to coherence conditions that need to be satisfied. We consider some possible solutions involving the use Aczel-style universes, and having explicit transport maps instead of type equalities.
B-systems - a link which connects the syntax of dependent type theories with their semantics