Monthly Archives: October 2018

#HoTT Sets in homotopy type theory (Bas Spitters)

Henosophia TOPOSOPHIA μαθεσις uni√ersalis τοποσοφια MATHESIS οντοποσοφια ενοσοφια Philosophie, théorie des catégories et théorie homotopique des types

Page 20 hiérarchie de la complexité

Niveau -2 : les types A contractiles cad tels que le type isContr(A) dont la formule est donnée page 20 ait au moins un terme (soit habité)

Niveau -1 : le type A est une pure proposition , cad isProp(A) est habité

Niveau 0 : les ensembles , cad les types A t q isSet(A) est habité

Le h-level (homotopy level ) est le niveau précédent auquel on ajoute 2

Les types contractibles sont de h-level…

https://ncatlab.org/nlab/show/contractible+type

Les ensembles sont les types de h-level 2

Voir le tableau de correspondance en paragraphe 2 de

https://ncatlab.org/nlab/show/homotopy+level

Les ensembles sont les h-sets (h-level 2)

https://ncatlab.org/nlab/show/h-set

Page 22 de http://www.cs.au.dk/~spitters/SpittersSets.pdf

Formule inductive (par récurrence )de définition de

Is-(n+1)-type (A) à partir de is-n-type(x=y)

Page 23, 24 : définition de l’équivalence puis de l’homotopie entre fonctions f,g : A ? B

f ∾ g est une relation appelée…

View original post 52 more words

Une théorie de l’homotopie est une catégorie simpliciale