PROGRAMME
Jeudi 27 juin, 9h30-13h (Bât. Condorcet, salle 366A) – François Métayer, “Introduction à l’algèbre homotopique”
Je présenterai les bases de l’algèbre homotopique du point de vue des catégories de modèles de Quillen. Je m’attacherai en particulier à préciser ce que veut dire construire un objet par recollement “à homotopie près”, ce qui nous conduira à dégager la notion fondamentale de colimite homotopique.
Jeudi 27 juin, 14h30-16h30 (Bât. Condorcet, salle 366A) – Discussions libres
Jeudi 27 juin, 16h30-18h30 (Bât. Condorcet, salle 366A) – Jean Petitot, “Phénoménologie et géométrie des esquisses perceptives”
A la demande des organisateurs, je parlerai de géométrie de la perception et, plus précisément, des déformations des contours apparents des objets. Philosophiquement, cela rejoint la phénoménologie des esquisses perceptives développée par Husserl.
Vendredi 28 juin, 9h30-13h (Bât. Condorcet, salle 366A) – Guillaume Brunerie, ” La notion d’égalité en théorie des types homotopiques”
Le but de cet exposé est de présenter divers aspects de la notion d’égalité en théorie des types homotopiques. On parlera entre autres de sa définition comme famille inductive de types, des surprenantes similarités avec la notion de chemin en théorie de l’homotopie, de l’axiome d’univalence, et de comment ses aspects homotopiques peuvent être compris au niveau des fondements des mathématiques.
Vendredi 28 juin, 14h30-16h30 (Bât. Condorcet, salle 366A) – Discussions libres
Vendredi 28 juin, 16h30-18h30 (Bât. Condorcet, salle 366A) – Luc Pellissier, “Déformation et orthogonalité : le point de vue de la géométrie de l’interaction”
La géométrie de l’interaction est un programme de recherche introduit par J.-Y. Girard à la fin des années 80, visant à caractériser les preuves et les programmes par delà de certaines déformations. Il mène à porter en son cœur une orthogonalité, forme raffinée de la négation.
Samedi 29 juin, 9h30-11h (Halle aux Farines, salle 237C) – Mathieu Anel, “Dépendances en géométrie”
Afin de comprendre ce qu’est la théorie homotopique des types, il est important de comprendre ce qu’elle n’est pas. Avant ses aspects homotopiques, le cœur de cette théorie est la théorie des types dépendants de Martin-Löf (MLTT). À l’aide d’exemples en géométrie, je vais tenter de faire comprendre ce qu’est une théorie de la dépendance. Je montrerai comment ces exemples possèdent plus ou moins de la structure de la MLTT (+,x,∑,∏,=,U,Bool,N,W…). Le paysage qui en résultera enrichira les interprétations classiques de la MLTT en termes d’ensembles et d’∞-groupoïdes.
Samedi 29 juin, 11h30-13h (Halle aux Farines, salle 237C) – Brice Halimi et David Rabouin, “Le concept d’homotopie : perspectives historiques et philosophiques”
Les mathématiques identifient souvent leurs objets à quelque chose près : par exemple à isomorphisme près en théorie des ensembles, à équivalence d’homotopie près en topologie algébrique. Cette identification est-elle une identification d’objets différents, par oubli de déterminations jugées non pertinentes, ou bien une identification qui donne originairement son identité à chaque objet? On peut parler d’identification-modulo dans le premier cas, et de donation d’identité dans le second.
Une identification-modulo, contrairement à une donation d’identité, fait apparemment référence à un niveau absolu d’identité au moins supposé (même s’il n’est pas explicité). C’est pourquoi les questions d’identification en mathématiques sont souvent abordées à partir d’une forme absolue d’identification attribuée à Leibniz au titre du “principe des indiscernables” : deux entités sont identiques si et seulement si elles partagent toutes les propriétés. La manière dont on formalise ce principe et dont on rend l’idée de “propriétés” a des conséquences importantes pour trancher certains débats philosophiques, comme ceux qui touchent aux interprétations “logicistes” ou “structuralistes”.
Dans cet exposé, nous voudrions revenir sur ces questions d’un point de vue historique et épistémologique afin de dénouer certains malentendus, en commençant par distinguer les deux types d’identification mentionnés.