#HoTT : Comprehension categories as models of type theory

D’abord cet article axé sur les « comprehension categories « :

http://www.cs.nott.ac.uk/~psxpc2/report-2013.pdf

puis cet exposé de Michael Shulman :

https://home.sandiego.edu/~shulman/hottseminar2012/05categories.pdf

(Cf page 3 la définition de display map category)

Et cet autre article :

https://ac.els-cdn.com/S1571066108000431/1-s2.0-S1571066108000431-main.pdf?_tid=6ae513c2-45bf-4641-820e-85f126850e32&acdnat=1520157026_ef815d3183b0c1afb49272a9aa0c2e4a

http://enslyon.free.fr/rapports/info/Alexandre_Buisse_3.pdf

http://philomatica.org/wp-content/uploads/2016/12/models.pdf

La méthode la plus simple consiste à partir des catégories cartésiennes fermées :

https://mathesismessianisme.wordpress.com/2015/08/28/ccc-cartesian-closed-category-categories-cartesiennes-fermees/

https://hottandphilosophy.wordpress.com/2017/11/18/univalence-in-locally-cartesian-closed-categories/

https://anthroposophiephilosophieetscience.wordpress.com/2018/01/06/chris-kapulkin-type-theory-and-locally-cartesian-closed/

La notion de type dépendant aboutit à la notion de contexte d’un théorème, ou d’une affirmation, c’est à dire une liste de noms de variables , de termes dans un type

Les tribus de Joyal (tribes) sont étroitement associées aux « comprehension categories » :

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/15/hott-relation-des-tribes-et-des-comprehension-categories/

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/15/categorical-models-of-dependent-types/

Une expression x:A est dite contexte d’un jugement :

x:A ⊢ B(x): Type

Voir Page 9 de

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

Les contextes sont introduits à partir de la page 6 dans

http://www.cs.nott.ac.uk/~psxpc2/report-2013.pdf

Ils forment une catégorie (hypothèse naturelle). Un objet terminal de cette catégorie est appelé contexte vide, ce qui correspond au cas où il n’y a pas d’hypothèses .

Étant donné un contexte Γ, une extension de Γ sera notée :

Γ.σ

Résultat de l’addition d’une variable de type σ au contexte Γ

Un morphisme Γ.σ → Γ

Est appelé « display map » , compris comme une interprétation de l’extension de contexte dans le contexte de départ en « oubliant » la nouvelle variable .

Cela correspond à un objet dans la slice category C/Γ

On parle de type σ sur (over) le contexte Γ.

Un terme M de type σ est un morphisme :

M : Γ → Γ.σ

Ce sera une section, un inverse à droite de la « display map » ci dessus

pσ ° M= 1

L’idée de cette définition est qu’un tel terme donne exactement l’interprétation de l’extension de contexte dans le contexte déc départ.

On aura un jugement selon lequel M est un terme de type σ :

Γ ⊢ M :σ

L’idée de substitution

Cet article

http://www.cs.nott.ac.uk/~psxpc2/report-2013.pdf

est précieux parce qu’il permet de retrouver l’idée qui est derrière les dispositifs mathématiques.
On comprend un morphisme entre deux contextes :

f: Δ → Γ

comme une interprétation des conditions (assumptions) de Δ en termes de celles de Γ; on cherche donc un moyen de transporter les types et termes sur Γ vers types et termes sur Δ

On cherche donc un type f*σ sur Δ avec un morphisme :

q(f,σ) : Δ.f*σ → Γ.σ

Ce morphisme sera appelé f étendu par σ

Cela , cette possibilité de transport, est garanti par l’existence d’un carré de produit fibré (pullback square) représenté sur la figure 1.2 page 9

http://www.cs.nott.ac.uk/~psxpc2/report-2013.pdf

https://en.m.wikipedia.org/wiki/Pullback_(category_theory)

Si la catégorie C des contextes est munie de pullbaks (produits fibrés) alors tout morphisme
f : Δ → Γ

détermine un foncteur entre les slice catégories correspondant aux deux objets de C que sont les contextes:

f* : C/Γ → C/Δ

Ce foncteur est appelé pullback ou de substitution ou de réindexation. C’est le même que celui qu’André Joyal appelle « foncteur de changement de base (base change functor) et qu’il décrit dans ses exposés sur l’interaction entre théorie des catégories et HoTT , par exemple :

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

page 28 sur 39 : product along a fibration

https://hottandphilosophy.wordpress.com/2018/01/30/base-change/

Ensuite, pages 9 sq de

http://www.cs.nott.ac.uk/~psxpc2/report-2013.pdf

on définit étant donné deux types σ et τ sur un même contexte leur produit dépendant qui est le type des fonctions

σ → τ

et leur somme dépendante ( dependent product, dependent sum)

Les termes du produit dépendant

Πστ

s’interprètent comme des fonctions dont le type résultat dépend de l’argument

On en vient à s’intéresser au foncteur adjoint à droite du foncteur de substitution qui a été décrit ci dessus, sans pouvoir être plus précis pour l’instant, comme cela est expliqué dans l’article à la fin de la page 8. D’où la définition 1.1.2 page 9

Un morphisme dans une catégorie munie de pullbacks (ici ce sera la catégorie C des contextes):
f: Δ → Γ
est dit exponentiable si le foncteur de substitution :

f* : C/Γ → C/Δ

possède un adjoint à droite

Joyal donne les mêmes conditions d’adjonction dans ses notes:

https://anthroposophiephilosophieetscience.wordpress.com/2018/01/20/differentes-notes-dandre-joyal-sur-la-description-categorique-de-hott/

ce qui est heureux !!

Cet ancien article est lié à celui ci :

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/15/categorical-models-of-dependent-types/

Ainsi que :

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/15/hott-relation-des-tribes-et-des-comprehension-categories/

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