Kapulkin : Π-types and Σ-types in homotopy theoretic models of type theory

Les types dépendants sont abordés dans le Livre, voir :

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/16/hott-the-book-1-4-dependent-function-types-π-types/

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

Ce travail de Kapulkin sous forme de transparents aborde le lien avec les catégories:

https://www.mathstat.dal.ca/~selinger/ofest2010/slides/Kapulkin-Pi_and_Sigma_slides.pdf

La page 3 sur 17 donne les équivalences pour Π et Σ dans les trois domaines de la théorie des types, de celle des ensembles ( où les correspondants sont le produit cartésien et le coproduit) et la logique ( où ce sont les deux quantificateurs, universel et existentiel, qui correspondent respectivement au
Π Et Σ-type)

Les deux pages suivantes (4 et 5) donnent les règles de formation, d’introduction, d’élimination et de calcul (COMP) respectivement pour les Π et Σ-types.

Un exemple de formation est donné Page 6 suivante pour le type Nat des entiers naturels et le type dérivé:

n:Nat ⊢ Rn: Type

Puis les notes abordent la sémantique des Lccc ( locally cartesian closed categories)

https://proofwiki.org/wiki/Definition:Pullback_Functor

Les catégories localement cartésiennes fermées sont aussi expliquées (Page 20) dans cette note d’André Joyal:

http://www.math.uwaterloo.ca/~asl2013/Slides/Joyal.pdf

A tout morphisme :

f: B → A

on associe le « foncteur pullback le long de f  «  entre les « slice categories « :

Δf : C/A → C/B

et ce foncteur possède dans certains cas un adjoint à gauche et à droite :

Σf ⊣ Δf ⊣ Π f

Une catégorie munie des limites finies (pour un nombre fini d’objets ) est dite localement cartésienne fermées si l’adjoint à droite existe pour tout morphisme f (Page 8).

Le théorème de la page 12 sur 17 orienté vers les catégories C qui ont une structure de « model category »: ces catégories satisfaisant de conditions supplémentaires précisées Page 12 possèdent des modèles pour les Π-types.

Trois exemples de telles catégories sont donnés ensuite : la catégorie Grpd des groupoides, la catégorie Sset des ensembles simpliciaux, et la catégorie Preord des préordres

Page 14 est rappelé que la catégorie des préfaisceaux simpliciaux est un modèle de la théorie des types de Martin Lof.

https://ncatlab.org/nlab/show/simplicial+presheaf

https://ncatlab.org/nlab/show/model+structure+on+simplicial+presheaves

https://ncatlab.org/nlab/show/local+model+structure+on+simplicial+presheaves

https://hal.archives-ouvertes.fr/hal-00772850/document

http://www.konradvoelkel.com/2012/11/simplicial-presheaves-model/

Advertisements
This entry was posted in ∞-catégories, category theory, Higher category theory, Homotopy, homotopy type theory, Science-internelle. Bookmark the permalink.