Théorie homotopique des types

Carte Commune · n° 383035

Dans la logique mathématique et de l'informatique, la théorie homotopique des types ou plus exactement la théorie des types d'homotopie (en anglais Homotopy Type Theory, ou 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...

Lire sur Wikipédia · Image Presented at https://github.com/HoTT/book, CC BY-SA 3.0