Cet article trace le parallèle entre le livre « Homotopy type theory Univalent foundations »:
https://aperiodical.com/2013/06/homotopy-type-theory-a-new-foundation-for-21st-century-mathematics/
Et les « Principia mathematica » de Whitehead et Russell, qui fonde les mathématiques du siècle dernier, et qui est ici :
https://quod.lib.umich.edu/u/umhistmath/aat3201.0001.001/23?view=image&size=100
(En forme très aisée pour la lecture)
https://ncatlab.org/nlab/show/Principia+Mathematica
L’article rappelle qu’il a fallu aux PM 379 pages pour prouver que 1+1=2, tandis que les 250 premières pages du livre HoTT suffisent pour déduire les groupes d’homotopie des sphères à partir des bases de la théorie des types.
Cette page relie HoTT aux théorèmes d’incompletude De Godel, qui datent de 1931, vingt après les Principia mathematica qui sont de 1910:
Le langage formel des Principia mathematica est identique à la théorie des types, inventée par Russell :
https://www.sciencedirect.com/topics/computer-science/principia-mathematica
http://www.nuprl.org/documents/Constable/PrincipiaArticle.pdf
La notation, le langage formel, des Principia peut être étudié ici :
