Une rose seule, c'est toutes les roses et celle-ci : l'irremplaçable, le parfait, le souple vocable encadré par le texte des choses. Comment jamais dire sans elle ce que furent nos espérances, et les tendres intermittences dans la partance continuelle.
La théorie des types émerge des travaux de Bertrand Russell , au début du 20eme siècle, elle atteint des niveaux plus sophistiqués dans les recherches de logiciens comme Alonso Chirch , HoTT en est le stade le plus moderne ( début du 21 éme siècle ) et constitue une nouvelle manière de fonder toutes les mathématiques.
HoTT (homotopy type theory) se situe au croisement de l’homotopie, de la théorie des ∞-catégories, de la logique mathématique et de la Science des ordinateurs (« computer Science »).
L’article suivant fait le point sur ces applications pratiques:
La définition importante (Page 13-14 sur 81) est celle de tribu (« tribe « ) , c’est à dire une catégorie C munie d’une structur de tribu F (une sous-catégorie F de C) et d’un objet terminal.
Les morphismes de F sont appelés fibrations.
Les types sont les objets E d’une tribu C, noté
⊢E : type
Un terme de type E est un morphisme :
* ? E
où * est l’objet terminal
(Dans la théorie des catégories les flèches de l’objet terminal vers un objet quelconque A sont appelés éléments de A si A est un ensemble, ils se confondent avec les éléments de A au sens ensembliste)
Des exemples de tribus ( avec un choix adéquat des fibrations ) sont donnés Page 15:
notamment la catégorie Grpd des ( petits) groupoides, la catégorie Kan des complexes de Kan
HENOSOPHIA τοποσοφια μαθεσις υνι√ερσαλις οντοποσοφια 