#HoTT analogie des n-types et des n-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 ενοσοφια μαθεσις

Revenant à l’article séminal de Michael Shulman:

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

il aborde page 9 section 5 (« identification and equivalences « ) la notion de n-types qui forment à partir de n= -2 une échelle infinie semblable à la table périodique des n-catégories :

https://anthroposophiephilosophieetscience.wordpress.com/2017/01/17/scienceinternelle-7-la-table-periodique-des-n-categories/

Ainsi , comme pour les n-catégories, les 0-types (n=0) sont les ensembles, il n’y a qu’un seul n-type pour n=-2’qui est le singleton {1}, pour n=-1il y a deux -1-types qui s’identifient aux deux valeurs de vérité 0 et 1, et l’induction (la récurrence ) s’effectue ainsi :

A est un-type si pour tout x:A et y:A le type x=y est un (n-1)-type

L’axiome d’univalence de Voevodsky  » les objets isomorphes sont égaux » encode exactement le principe fondateur du structuralisme.
Ainsi , si l’on dénote par U le type total, appelé « Univers » , le type des ensembles est un sous-type de l’univers qui contient seulement les ensembles , c’est…

View original post 319 mots de plus

Publicités