Awodey : cubical #HoTT 1

http://www.helsinki.fi/lc2015/materials/slides_awodey.pdf

Il n’est pas question ici de se lancer dans les arcanes des “cubical sets” et des recherches récentes sur la “cubical HoTT”, à la fin de cette note, mais de comparer les pages du début à celles du travail d’André Joyal , inspiré de la théorie des catégories, dans l’article précédent.
Ainsi la Page 4 sur 53 chez Awodey explique les entités de base, les types et leur éléments les termes , elle est à comparer à la Page 15 du travail de Joyal , mais la notion de “dependent types ” est plus claire, je trouve, chez Joyal, de même d’ailleurs que les notions de types et de termes: ce sont des objets de catégories qui sont des tribus. Et un “dependent type” est un objet d’une catégories appelée “tribu locale” , définie page 17 sur 81 chez Joyal.

La Page 5 sur 53 de l’article d’Awodey explique la notion très importante de correspondance de Curry-Howard , qui revient régulièrement, sous la forme d’un tableau , en deux lignes, très clair:

https://en.m.wikipedia.org/wiki/Curry–Howard_correspondence

Les types sont à comprendre, non plus comme des objets dans des catégories, mais comme des propositions, une notion de logique donc : et si un type est vu comme une proposition, les termes de ce type, qui mathématiquement sont des éléments de ce type considéré comme une sorte d’ensemble, sont des preuves mathématiques de cette proposition, c’est à dire analogues à des programmes informatiques.

Mais quel est le statut des équations sur un type À, présentées page 4 sur 53 ?

s= t : A

par rapport aux “Identity types” présentés page 7 sur 53 ?

La question est d’ailleurs posée Page 7 : quels sont les termes de ces “Identity types” ?
Certes, sur le versant logique ( un type est une proposition) la réponse est claire : un “Identity type” noté:

Id A ( x, y )

Est la proposition : x= y

Mais sur le versant mathématique de la correspondance de Curry-Howard ?

Les trois pages suivantes (“Homotopy interpretation”) donnent des indications : les types sont interprétés comme des espaces, les termes comme des fonctions (“maps”)

a : A est interprété comme : a est un point de A

C’est à dire que a est un morphisme :

a : 1 → A

Les termes des “Identity types” sont des chemins menant d’un point à un autre , et donc les “Identity types” sont, dans l’interprétation homotopique , des “espaces de chemins ” (“path Spaces” Page 9 sur 53

L’idée est d’interpréter :

p : Id X (a,b)

Comme : p est un chemin menant du point a au point b dans l’espace X

À partir de la Page 10 l’interprétation géométrique (homotopique ) est poussée de façon à aboutir aux structure de groupoide , et finalement (Page 13) un type est identique à un

∞-groupoide

Dont les k-morphismes successifs sont les termes, les identités entre les termes, les identités entre les identités, (des homotopies) et ainsi de suite…

La Page 14 sur 53 (“Voevodsky n-types” ) introduit de nouveaux termes , à retenir :

Un type est contractile s’il a un terme. Un type est une proposition s’il a au plus un terme (s’il a 0 ou 1 terme , dans le cas où il a 0 terme c’est une proposition vide de sens ou fausse) , un type est un ensemble (Set) si l’égalité entre termes (qui est un type) est toujours une proposition, c’est un 1-type si l’identité entre identités est toujours une proposition, etc.. Page 15 nous retrouvons la hiérarchie des n-types, semblable à celle des n-catégories:

https://anthroposophiephilosophieetscience.wordpress.com/2017/08/06/hott-analogie-des-n-types-et-des-n-categories/

Advertisements
This entry was posted in homotopy type theory and tagged , , . Bookmark the permalink.