Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.

Constructive mathematics and models of type theory

Dates and location

From June 2 to June 6, at Institut Henri Poincaré.

Presentation

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.

Lectures

  • 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
  • P. Dybjer (TH Chalmers Gothenburg) : What is a model of intuitionistic type theory
  • M. Hofmann (LMU Munich) : Revisiting the categorical interpretation of 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
  • G. Munch-Maccagnoni (Univ. Paris 7) : Polarities and classical constructiveness
  • 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

Planning

Monday 2 June
10h30-12h00Per Martin-LöfSample space-time
14h00-15h30Peter DybjerWhat is a model of intuitionistic type theory
16h00-17h30Steve AwodeyNatural Models of Type Theory
Tuesday 3 June
10h30-12h00André JoyalCategorical homotopical logic
14h00-15h30Erik PalmgrenModels of dependent types and dependently typed logic and their formalization in type theory
Wednesday 4 June
10h30-12h00Guillaume Munch-MaccagnoniPolarities and classical constructiveness
14h00-15h30Joachim KockUnivalence in locally cartesian closed infinity-category
16h00-17h30Martin HofmannRevisiting the categorical interpretation of type theory
Thursday 5 June
10h30-12h00Denis-Charles CisinskiUnivalence for elegant models of homotopy types
14h00-15h30Ronnie BrownIntuitions for cubical models of homotopy types
16h00-17h30Simon HuberA Model of Type Theory in Cubical Sets
Friday 6 June
10h30-12h00Andrej BauerConstructive Model Categories
14h00-15h30Vladimir VoevodskyB-systems - a link which connects the syntax of dependent type theories with their semantics

Abstracts

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.

Hofmann
Revisiting the categorical interpretation of type theory

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

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

workshop_2.txt · Last modified: 2014/05/30 06:45 by mellies
Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.
www.chimeric.de Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0