HoTT = théorie homotopique des types, pas théorie des types homotopiques. C'est une version de la théorie des types, théorie qui se situe grosso modo comme un langage basique commun pour les maths, la logique et l'info.