Cerise.moe

Comodalités, adjoints dépendants et univers (23/10/18)

(D'après Licata, Orton, Pitts, Spitters)

Une comodalité, en logique modale, est donnée par des règles de type comonade :

Comme les (co)monades sont « essentiellement » la même chose que les adjonctions, et que l'on souhaite obtenir l'équivalent des comodalités en théorie des types dépendants, on s'intéresse aux adjonctions chez les types dépendants.

Comme la théorie des types dépendants est moralement l'étude des catégories LCCC, on aimerait transformer l'équation fondamentale de l'adjonction en
LΓ ⊢ A ≅ Γ ⊢ RA
d'une manière cohérente sur les éléments.

Ça peut sembler bizarre parce que Γ ⊢ A ça veut dire Γ, A → Γ donc l'adjonction semble être dans le mauvais sens. Mais c'est parce que ce sont les sections qui nous intéressent, pour lesquelles Γ est bien le domaine.

On utilise des CwF pour formuler ça de manière précise. Ça devient :

Dans la syntaxe, on peut modéliser ça par :

Il est naturellement possible d'obtenir de telles adjonctions en partant d'une adjonction dans une LCCC. Naïvement, on a envie de construire une CwF en prenant les flèches de la LCCC, mais on sait que ça ne marche pas bien sans choisir des « display maps ».

Pour remédier à cela, on triche en prenant des flèches généralisées :
A               A
↓  devient      ↓
Γ           Γ → Δ

Comme le pullback est alors remplacé par une composition, tout est associatif « on the nose ». Cette construction (catégorie de Giraud GC) donne un foncteur pleinement fidèle dpuis les catégories Lex vers les CwF. C'est un adjoint au foncteur d'oubli CwF → lex.

====

Un exemple d'utilisation est la construction d'univers dans le modèle Orton & Pitts.

On peut commencer par noter que la notion naïve d'univers est incohérente. En effet, supposons que l'on aie un univers U tel qu'une flèche Γ → U soit la même chose qu'une fibration sur Γ.
Alors, si l'on prend une fibration pointwise γ : I → A le long d'un chemin, en mettant I dans le contexte on obtient i : I ⊢ γ : A et donc un point de U dans le contexte i:I. Puis en faisant l'abstraction de i, on obtient un chemin I → U qui devient, par pullback, une fibration sur I. Cette fibration doit être égale à γ si les axiomes élémentaires de de classification sont respectés.
On a ainsi transformé une fibration pointwise en fibration globale. Or, il n'est pas très dur de construire une fibration pointwise qui n'est pas une fibration globale : par exemple [_ ≡ 0] sur I.

Cela peut être imputé à la construction des univers qui n'est pas assez uniforme : typiquement, la propriété de classification marche bien avec les transformations naturelles de codomaine U, mais plus du tout avec les Hom internes.
Pour remédier au problème, on peut enrichir le langage interne interne en lui autorisant à parler de sections globales, à l'aide d'une comodalité.

En effet, on a l'adjonction naturelle entre le foncteur de sections globales et le foncteur « préfaisceaux constant » :
Ĉ | cst ⊣ Γ | Set
On obtient donc naturellement une comonade cst∘Γ (notée L dans la suite) sur les préfaisceaux cubiques. LΓ, Δ ⊢ A signifie que toutes les variables dans Γ sont des sections globales.
On se rappelle que les sections globales sont données par les points, donc LΓ ⊢ A signifie que A vit au-dessus d'un h-set. J'imagine donc que l'adjoint à droite consiste à « saturer » les fibres au-dessus des cellules de dimensions supérieures : pour toute cellule c dans Γ, on met un élément par section Lc → A.

Maintenant, on peut s'en servir pour construire un univers.

====

Dans le modèle préfaisceaux cubiques, l'objet I est minuscule : le foncteur _^I a un adjoint à droite (en plus de l'adjoint à gauche donné par _×I).

Pour s'en convaincre, on se rappelle que I = y1, donc que _^I = (_×1)* et si on prend un préfaisceau F,
      F
    □ → Set
_×1 ↓
    □

l'extension de Kan de F selon ce diagramme vérifie
[(_×1)*G, F] ≅ [G, RF]
Comme la construction d'extensions de Kan est fonctorielle en tout ce que l'on souhaite, on obtient que R_ est adjoint à droite de (_×1)* = _^I (de même L_ est adjoint à gauche). On note l'adjoint à droite √_

Concrètement, je pense que ça se traduit par un shift de dimensions dans le sens opposé à _^I.
Malheureusement, contrairement à l'adjoint à gauche, celui à droite ne peut pas s'exprimer dans le langage des Hom internes. Mais notre comodalité rend cela possible ! On écrit ça à l'aide de deux nouveaux foncteurs L' ⊣ R' pour encoder cette nouvelle adjonction
L(A : Set, B : Set, f : A^I → B) ⊢ R'f : A → √B
L(A : Set, B : Set, f : A → √B) ⊢ L'f : A^I → B
etc

Ceci va nous servir à classifier correctement les objets classifiés par des sections Γ^I ⊢ A

====

Si on a A : Γ → Set une famille dépendante, les structures de fibration globales 1 → isFib A correspondent aux sections de π₁ : (p : Γ^I) × Comp(A∘p) → Γ^I.
(ie à chaque chemin p dans Γ^I on associe une structure de composition sur A∘p)

Donc les fibrations correspondent à des flèches Γ → √(p : Γ^I) × Comp(A∘p) qui sont des pseudo-sections de √π₁ (à un η près).
On arrive donc à classifier les fibrations sur une base donnée.

Pour en déduire un univers de fibrations :
Une structure de fibration sur Γ ⊢ A devient un carré commutatif
 Γ^I  →  Elt
  ↓       ↓
Set^I →  Set

où le morphisme horizontal du bas est Comp, et les morphismes verticaux sont A^I et la fibration naturelle sur Set.
(Prendre le chemin du bas associe à chaque chemin dans Γ l'ensemble des structures de composition, et prendre le chemin du haut revient à choisir une structure pour chaque chemin)
On en déduit un carré commutatif adjoint :
 Γ  →  √Elt
 ↓       ↓
Set →  √Set

où le morphisme vertical de gauche est A. Ces carrés sont clairement équivalents aux fibrations, et sont représentés par le pullback U de Set → √Set ← √Elt. Fin.