Théorie des Types Homotopiques (HoTT)

Un cadre fondateur qui interprète la théorie des types de manière homotopique : les types sont vus comme des espaces (ou ∞-groupoïdes), les termes comme des points et les égalités comme des chemins, mariant les constructeurs typés logiques à une sémantique homotopique.