- Tuesday April 16, 14h00-17h00, room 1020 Sophie Germain
- Thursday April 18, 9h00-12h00, room 1020 Sophie Germain
- Tuesday April 23, 9h00-12h00, room 266 Olympe de Gouges
- Thursday April 25, 9h00-12h00, salle 2012 Sophie Germain
- La correspondance de Curry-Howard
- une correspondance entre syntaxe intrinsèque et extrinsèque
- propositions vues comme types « proof-irrelevant »
- Comparaison entre types simples et types dépendants
- la correspondance fibrée/indexée
- Comparaison avec la théorie des ensembles
- intrication calcul/logique (à la Church, à la ML, à la théorie des types) vs séparation totale calcul/logique (à la Curry, à la Lisp, à la ZF)
- les ensembles vus comme arbres inductifs ou coinductifs (les ensemble de Aczel)
- La théorie des types comme jeu de légo
- les différents types : ∑, Π, =, inductifs, coinductifs, troncation, univers
- les règles de construction : formation, introduction, élimination, β-réduction, η-conversion
- Les différentes formes d'égalité
- intensionnelle/extensionnelle
- définitionnelle/propositionnelle
- Implémentations de la théorie des types
- comparaison entre les logiques d'Agda, Coq, Isabelle, Lean, Mizar, ...
- décidabilité de l'égalité définitionnelle
- Exercices
- Type = espace à homotopie près, égalité = chemin
- h-niveaux de Voevodsky
- une reconstruction des propositions, ensembles, groupoïdes comme types
- Les types inductifs supérieurs
- exemples du cercle et de la sphère (homotopie synthétique)
- exemple des types quotients
- Le principe d'univalence
- différentes définitions d'équivalence
- l'univalence comme principe d'extensionnalité généralisation l'extensionnalité des propositions
- Axiome du choix
- l'axiome du choix « intensionnel » de Martin-Löf
- l'axiome du choix général comme distribution du produit dépendant sur la troncation
- prouvabilité du choix unique
- l'axiome du choix général implique la logique classique (théorème de Diaconescu)
- Exercices
- La correspondance Curry-Howard-Lambek et son extension à la géométrie
- Un modèle « syntaxique » : les catégories avec familles
- L'interprétation des types dépendants comme « fibrations »
- Catégories cartésiennes localement fermées
- Les correspondances intrinsèque/extrinsèque, fibrée/indexée, classe de structures/structure initiale en action
- Univers vus comme classificateur d'objets
- ∞-catégories et ∞-groupoïdes
- Les différentes formes géométriques
- globes (= itération de l'égalité homogène)
- triangles/simplexes
- cubes (= itération de l'égalité hétérogène)
- opétopes
- Les différents équipements de structures
- l'infrastructure pure de dépendances (structure « semi- »)
- dégénérescences = réflexivités = identités
- complétion des cornets internes = transitivité = composition (structure de Kan faible)
- complétion de tous les cornets = ajout de symétries = ajout d'inverses (structure de Kan forte)
- Exercices
- Les preuves d'égalité sur un type vues comme chemins formels, fonctions d'un intervalle formel vers le type
- Diverses propriétés possibles pour l'intervalle formel
- Les fonctions sur types inductifs supérieurs comme fonctions réécrivant des preuves d'égalités
- Exemples de raisonnement égalitaire en théorie des types cubiques
- Substitutivité de l'égalité par complétion de cubes ouvert (composition de Kan)
- L'univalence comme algorithme de réécriture de preuves sur une structure en preuves sur structures équivalentes
- Paramétricité et réalisabilité au cœur de la correspondance intrinsèque/extrinsèque
- La paramétricité itérée comme génératrice des ensembles simpliciaux et cubiques
- Comparaison avec la théorie des types observationnelle supérieure
- Exercices
Le cours, fait au tableau, laissera cependant la place à l'improvisation en fonction des demandes de l'auditoire.
- HoTT Book, 2013
- Homotopy type theory: the logic of space, Michael Shulman, 2017
- Introduction to homotopy type theory, Egbert Rijke, 2018
- Pierre-Louis Curien's LMFI lectures on the syntax of Martin-Löf's type theory, the categorical interpretation of extensional type theory and homotopy type theory
- A HoTT library in Coq
- A HoTT library in Agda
- The UniMath library for "Univalent Foundations" in Coq
- Set theory in type theory
- Martin-Löf’s Type Theory, B. Nordström, K. Petersson and J. M. Smith, 2000
- Constructing Quotient Inductive-Inductive Types, Ambrus Kaposi, András Kovács, Thorsten Altenkirch