#HoTT simplicial set model of type theory : types as Kan complexes

Dans la note déjà étudiée :

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

André Joyal cite page 17 sur 39 les travaux d’Awodey, Warren et Voevodsky sur les modèles de la théorie des types dans les ensembles simpliciaux

Les types, objets de base de TT , sont vus comme des complexes de Kan, et leurs termes (éléments ) comme les sommets de ces complexes

Un complexe de Kan est, comme une quasicatégorie, un cas particulier d’ensemble simpliciaux, c’est à dire d’objet du topos Sset, voir cet ancien article :

https://anthroposophiephilosophieetscience.wordpress.com/2018/04/02/eva-belmont-simplicial-sets-and-quasicategories/

et le lien d’Eva Belmont :

https://math.mit.edu/~ebelmont/ssets.pdf

qui a le mérite de réintroduire les ∞-catégories, et aussi les quasicatégories : Qcat, catégorie des quasictégories, est un ∞-cosmos, c’est à dire un univers dont les objets sont les ∞-catégories, un mathème du plan internel des Idées, dit « Étendue intelligible »

La note de Joyal :

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

poursuit pages 17 et 18 sur le modèle de la théorie des types dans la catégorie des ensembles simpliciaux, plus particulièrement les complexes de Kan :

Un type dépendant en contexte A est (a pour modèle ) une fibration :

E ↠ À

C’est une fibration de Kan dans le cas où le modèle est celui de complexes de Kan:

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

La page 18 présente la « preuve diagrammatique » , un carré de pullback :

Une fibration E ↠ À peut être vue comme une famille (E(x) : x ∊ À) d’objrts Indexés par un élément variable x de A ( c’est à dire un morphisme dirigé de 1 vers À, où 1 est l’objet terminal de la catégorie)

Ce qui est la définition d’un type dépendant en contexte A.

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

Leave a Reply

Please log in using one of these methods to post your comment:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s