André Joyal : categorical #HoTT 3

Nous poursuivons l’étude de la précieuse conférence de Joyal qui est ici :

https://ncatlab.org/homotopytypetheory/files/Joyal.pdf

Il est tout à fait utile d’étudier ce texte en même temps que le Big Book de HoTT pour garder le parallèle des notions catégoriques ( sur lesquelles insiste Joyal) et des notions plus spécifiques à HoTT qui tournent autour des types et de leurs termes ou éléments ainsi pour prendre un exemple la notion de “dependent type ” dans un contexte x : A correspond (Page 17 sur 81) à un objet (E,p) d’une tribu locale C(A) , notion définie à la même page 17. Donc nous avons, en étudiant en parallèle les deux, une sorte de registre traduisant les deux langages l’un dans l’autre, une “Pierre de Rosette” en quelque sorte.

Le concept de “changement de base” (“base change”) est présenté page 12, il donne lieu (Page 21) à un foncteur entre tribus locales:

f* : C(B) → C(A)

qui correspond à une règle de déduction en logique de la théorie des types .

Ainsi l’exercice de traduction entre les deux registres ( théorie des catégories vs théorie des types) continue.

La Page 22 est un cas particulier “restriction of context ” , en faisant B=* (objet terminal de la tribu C) dans la carré de la Page 12.
On obtient un foncteur iA: C → C(A)

qui correspond à une règle de déduction appelée en théorie des types “affaiblissement de contexte”. Ainsi une règle en théorie des types correspond à un foncteur en théorie des catégories .

Page 25:

L’espace total (“total Space”) d’une fibration p : E → A

est noté ∑x:AE(x)

et l’on note cette opération de sommation:

A : C(A) → C

Associée au foncteur d’oubli de la tribu locale C(A) vers C

Selon la définition d’une tribu locale Page 17, il est aisé de comprendre qu’un foncteur d’oubli de cette sous catégorie de C/A consiste à ” oublier” tout ce qui est du domaine de À, qui est un objet de la catégorie C.

Encore une fois une règle logique, la règle de ∑-formation, correspond à ce foncteur .

Un terme de ce nouveau type

t: ∑x:A E(x)

est une pire (a,u) comme décrit Page 25′ où :
a : A et u : E(a)

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