Michael Shulman

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 homotopique des types 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.