#HoTT et théorie des catégories

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://benedikt-ahrens.de/talks/Marseille.pdf

Les types, entités qui sont à la base de HoTT et y remplacent les ensembles (ensembles qui sont considérés comme des types particuliers) peuvent être considérés comme des ∞-groupoides.

L’axiome des « univalent foundations  » asserte en gros que pour les types, isomorphisme coïncide avec égalité. L’axiome est noté en abrégé U F et accompagné toujours l’Homotopy type theory qu’on note donc quelquefois en abrégé HoTT UF

HoTT interprète les types comme des espaces (Page 9 sur 67) les éléments d’un type a:A sont interprétés comme des points dans un espace (Page 10 sur 67).
Une attention spéciale doit être portée aux « Identity types » qui sont dans HoTT le représentant du principe d’unité qui dans les catégories est le morphisme identité et que Badiou interprète pour les ensembles comme « compte pour un »

Pour deux éléments de type A a,b:A il existe un type d’identité (  » Identity type ») qui est…

View original post 294 mots de plus

Publicités