Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.
Concept
Théorie des types homotopiques
Résumé
vignette| Couverture de la Théorie des types homotopiques : Fondations univalentes des mathématiques.
Dans la logique mathématique et de l’informatique, la théorie des types homotopiques (en anglais : Homotopy Type Theory HoTT) fait référence à différentes lignes de développement de la théorie des types intuitionnistes, basée sur l’interprétation des types comme des objets auxquels l’intuition de la théorie de l’homotopie s’applique.
Cela inclut, entre autres travaux, la construction de modèles homotopiques et de modèles de catégories supérieures pour de telles théories de types, l’utilisation de la théorie des types en tant que logique pour la théorie de l’homotopie et la théorie des catégories supérieures, le développement des mathématiques dans une base théorique de type (incluant à la fois les mathématiques existantes et les mathématiques rendues possibles par les types homotopiques), et la formalisation de chacune d’elles en assistants de preuve informatique.
Il existe un important chevauchement entre les travaux associés à la théorie des types homotopiques et ceux qui se réfèrent au projet des fondations univalentes. Bien que ni l’un ni l’autre ne soient définis avec précision et que les termes soient parfois utilisés de manière interchangeable, l’utilisation correspond parfois à des différences de points de vue et de priorités. En tant que tel, cet article peut ne pas représenter de manière égale les points de vue de tous les chercheurs dans ces domaines. Ce type de variabilité est inévitable lorsqu’un champ est en pleine évolution.
À une époque, l’idée que les types de la théorie des types intensive, avec leurs types identité, pouvaient être considérés comme des groupoïdes relevait du folklore mathématique. Elle a été précisée pour la première fois, de manière sémantique, dans l’article paru en 1998 de Martin Hofmann et Thomas Streicher, intitulé « The groupoid interpretation of type theory », dans lequel ils montraient que la théorie des types intensifs avait un modèle dans la catégorie des groupoïdes.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.