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

Autrement qu'être Mathesis uni∜ersalis Problema Universale Heidegger/Husserl être/conscience : plan vital-ontologique vs plan spirituel d'immanence CLAVIS UNIVERSALIS HENOSOPHIA PANSOPHIA ενοσοφια μαθεσις

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

View original post

Publicités