Axiomatic cohesion in 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 ενοσοφια μαθεσις

J’ai déjà parlé de cet article de blog, qui fait le lien entre les travaux de Lawvere sur « axiomatic cohesion « et l’homotopy type theory, à laquelle est associée de manière solidela théorie des ∞-catégories et ∞-topoi:

Axiomatic cohesion in HoTT

La correspondance est étudiée par le biais de la notion de langage interne qui est bien connue pour ce qui est des topoi ordinaires sous le nom de « langage de Mitchell-Benabou » et associée à la théorie extensinnelle des types :

https://ncatlab.org/nlab/show/extensional+type+theory

qui est une des « versions » ou « variantes » de la théorie des types de Martin-Lof, nouvelle fondation des mathématiques:

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

https://ncatlab.org/nlab/show/Mitchell-Bénabou+language

language interne où les objets d’un topos s’identifient aux types.

Les chercheurs de pointe dans le domaine de HoTT , comme Mike Schulman rédacteur de l’article, pensent que certains des (∞,1)-topoi de Lurie peuvent être identifiés aux topoi cohésifs de Schreiber, eux mêmes généralisation aux (∞,1)-topoi , qui unifiés « tous…

View original post 157 mots de plus

Publicités