HOTT: née de la confrontation de la théorie des types de Martin-Lof et de l’homotopie abstraite

http://home.sandiego.edu/~shulman/papers/synhott.pdf

La théorie de Martin-Lof est aussi appelée “dependent type theory” ou “intuitionnistic type theory”:

https://ncatlab.org/nlab/show/Martin-Löf+dependent+type+theory

https://en.m.wikipedia.org/wiki/Intuitionistic_type_theory

http://www.cse.chalmers.se/~bengt/papers/hlcs.pdf

Les types sont comme les ensembles des collections , mais qui se comportent différemment des ensembles :ils furent justement utilisés par Russell il y a plus d’un siècle pour pallier aux paradoxes et apories rencontrés (par Russell lui même ) en théorie des ensembles.
HoTT (homotopy type theory) est une Idée née vers 2006 indépendamment chez Awodey et Warren de l’intersection de la théorie des types, une branche de la logique mathématique, et de l’homotopie en même temps que de la “theoretical computer Science” : toutes les avancées dans ce fascinant nouveau domaine se trouvent sur le site:

https://homotopytypetheory.org

Advertisements
This entry was posted in Bertrand Russell, homotopy type theory, Philosophie mathématique, Théorie des ensembles (set theory) and tagged , , , , . Bookmark the permalink.