https://arxiv.org/abs/math/0212330
papier très important , Jacob Lurie précise en page 527 de HTT :
http://www.math.harvard.edu/~lurie/papers/highertopoi.pdf
« Our notion of ∞-topos is essentially equivalent to the notion of Segal topos introduced in the paper of Toen , Vezzosi and to Charles Rezk’s notion of model topos. We note Also That the paper of Toen, Vezzosi has considerable overlap with the ideas discussed here «
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 :
Les espaces sont les objets de l’ ∞-topos Spaces :
Le texte de Nima Rasekh est ici :
http://guests.mpim-bonn.mpg.de/rasekh/talks/PrelimPresentation.pdf
