Ensembles (sets) et #HoTT

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

Emily Riehl écrit sur Twitter que la conclusion de ce texte article de Mike Shulman « will blow your mind »:

« homotopy type theory : The Logic of space « 

https://arxiv.org/pdf/1703.03007.pdf

La théorie des « espaces synthétiques » est expliquée sommairement au début, il s’agit de ne pas considérer la notion d’espace comme une structure surimposée à une construction ensembliste ( exemple : les variétés différentielles sont des structures mathématiques, définies à l’aide d’atlas , sur des ensembles de points) mais directement comme des constructions alternatives aux ensembles, avec les points jouant le rôle des éléments pour les ensembles. Ceci est la tâche de la théorie constructionniste des types (dépendent type theory) de Martin Lof :

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

Ainsi, comme déjà noté, les types se présentent comme des collections de termes , analogues aux ensembles .
Comme d’autres systèmes formels, la theoriedes types de Martin Lof peut être interprétée dans des topos ou des « higher…

View original post 372 mots de plus

Publicités