Séminaire, 9 juin 2016
Programme
- 10:30 – 12:00
-
Thierry Coquand (University of Gothenburg (SE))Invited talk: Une justification de l’axiome d’univalence
Les travaux de Voevodsky suggèrent une extension de la théorie des types dependents qui résout certains problèmes de modularité (égalité extensionelle et quotients). Un problème est que la justification de cette extension est développée en utilisant le tiers-exclu et l’axiome du choix. Nous présentons un modele de cette extension dans un cadre constructif, et qui peut s’écrire avec avantage directement comme une théorie des types.
Des travaux récents de Christian Sattler (Leeds) montrent comment on peut utiliser ces idées pour décrire une structure de modele similaire a la structure de modele sur les ensembles simpliciaux, mais ou l’on n’utilise jamais le tiers-exclu et l’axiome du choix.
- 14:00 – 15:00
-
Guillaume Brunerie (Université Nice Sophia Antipolis)
Homotopy type theory (HoTT) is usually presented as Martin-Löf’s dependent type theory together with Voevodsky’s univalence axiom and various other axioms for higher inductive types. In particular, the presence of axioms makes it non-constructive in that one can find closed terms of type ℕ which do not reduce to canonical natural numbers. But with Thierry Coquand’s constructive cubical model, it becomes possible to compute with univalence and higher inductive types. In this talk, I will present various examples of such closed natural numbers that we would like to compute, extracted from the proof of π₄(S³)=ℤ/2ℤ in HoTT that I recently completed.
- 15:30 – 16:30
-
Thomas Streicher (Univ. Darmstadt (DE))
