André Joyal : #HoTT and category theory

Voici donc ce lien :

http://logica.dmi.unisa.it/tacl/wp-content/uploads/2014/08/Joyal-TACL2015.pdf

Récapitulons ce que nous avons déjà appris de Joyal sur les liens entre théorie des catégories et théorie homotopique des types:

Un type est un jugement, possibilité fondamentale de l’humain selon l’idéalisme contemporain qui est la philosophie amenant à la Science Internelle.

Cet acte de jugement vient sous deux formes:

Page 6 : l’assertion que A (par exemple N les entiers naturels) est un type , ce qui est noté:

⊢A : Type

Et Page 7 : l’assertion que x est un élément de type A

⊢x: A

Par exemple le jugement selon lequel 0 est un entier naturel:

⊢0: N

Les tribus (tribes) sont des catégories particulières, ayant certaines propriétés (Page 25)

Les types sont des objets de tribus. Les termes sont des éléments généralisés de ces objets, c’est à dire des flèches venant de l’objet terminal de la catégorie qu’est la tribu vers l’objet qui est le type .

Page 8 : un type dépendant (dependent type) est paramétré par un terme x de type A :

x:A ⊢B(x): Type

L’expression x:A à gauche du signe ⊢ est le « contexte » du jugement .
Un terme peut aussi dépendre de x :

x:A ⊢ t(x): B(x)

Plusieurs contextes peuvent être « concaténés »:

y: B(x), x:A ⊢ C(x,y): Type

Les règles de substitution sont expliquées en Page 9

Page 10 est expliquée la règle de formation de la somme (union disjointe) d’un type dépendant

Les règles de formation , d’introduction, d’élimination, de computation et d’unicité en pages 12 et 13 font référence aux explications du Livre sur HoTT en page 27:

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/27/hott-the-book-product-types-dependent-pair-types-ou-σ-type/

En page 13 sur 39 est développée la notion « equality type ou « identity type « : à un type A est associé un type EqA:

x,y:A ⊢ EqA(x,y): Type

Un terme p: EqA(x,y) est une preuve que x =y (Joyal utilise ce mot « preuve » alors que dans le Livre ils le déconseillent, lui préférant « évidence » ou « témoin »

Il y a deux modèles pour la théorie des types: celui des groupoides (Page 16) et celui des ensembles simpliciaux Page 17

Dans le premier les types sont vus comme des groupoides, les termes comme des objets de ces groupoides, les types dépendants en contexte A comme des fibrations de E vers A (Page 18) et les preuves que a ≃ b comme des isomorphismes a → b

Dans le second les types sont regardés comme des complexes de Kan

https://ncatlab.org/nlab/show/Kan+complex

les termes comme des sommets, les types dépendants en contexte A comme des fibrations de E vers A

https://en.m.wikipedia.org/wiki/Kan_fibration

et les preuves que a ≃ b comme des chemins de a vers b

Page 27 sur 39 : les tribus forment une catégorie qui est une 2-catégorie

Ce travail titré « Homotopy theory of type theories » vient à la suite , formalisant la notion de « catégories contextuelles »:

http://uwo.ca/math/faculty/kapulkin/papers/homotopy-theory-of-type-theories.pdf

Aussi les C-systemes de Voevodsky:

https://arxiv.org/abs/1409.7925

Advertisements
This entry was posted in ∞-catégories, ∞-topoi, homotopy type theory, Philosophie and tagged , . Bookmark the permalink.