Constructive mathematics and models of type theory

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.

• S. Awodey (CMU) : Natural models of type theory.
• A. Bauer (Univ. Ljubljana) : Constructive Model Categories
• R. Brown (Bangor Univ.) : Intuitions for cubical models of homotopy types
• D.-C. Cisinski (Univ. Toulouse) : Univalence for elegant models of homotopy types
• G. Munch (Univ. Paris 7) : Duality of computation and polarities
• P. Dybjer (TH Chalmers Gothenburg) : What is a model of intuitionistic type theory
• S. Huber (TH Chalmers Gothenburg) : A Model of Type Theory in Cubical Sets
• A. Joyal (Univ. Montreal) : Categorical homotopical logic
• J. Kock (Univ. Aut. Barcelona) : Univalence in locally cartesian closed infinity-category
• P. Martin-Löf (Univ. Stockholm) : Sample space-time
• E. Palmgren (Univ. Stockholm) : Models of dependent types and dependently typed logic and their formalization in type theory
• V. Voevodsky (Princeton) : B-systems - a link which connects the syntax of dependent type theories with their semantics

Awodey
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.

Bauer
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.

Brown
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. Cisinski
Univalence for elegant models of homotopy types Dybjer
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. Huber
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. Joyal
Categorical homotopical logic > Many aspects of homotopy (type) theory are best described in the language of category theory. What is an elementary infinity topos? Kock
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. Martin-Löf
Sample space-time Munch
Duality of computation and polarities > We shall review the duality of computation (Curien and Herbelin 2000) and its revisitation of the 2010's, by Guillaume Munch, and by Guillaume Munch and myself, under the light of polarities. In particular, we shall present Guillaume Munch's notion of duploid and we will sketch how it can be built upon to provide “direct” categorical models of polarised logics and of languages which allow for a mixture of call-by-name and call-by-value (ongoing work with Marcelo Fiore and Guillaume Munch). We shall also hint at some connections with operads. Palmgren
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. Voevodsky
B-systems - a link which connects the syntax of dependent type theories with their semantics ===== Organizers ===== * Thierry Coquand * Thomas Streicher