#HoTT André Joyal extension et restriction de contexte ; foncteurs logiques , termes génériques

http://www1.maths.leeds.ac.uk/~pmtng/HOMALG/joyal-mit.pdf

Un type est un objet E d’une tribu C, c’est à dire une catégorie satisfaisant certaines conditions cf page 13 sur 81:

⊢E : Type

Un terme est un élément d’un type E, c’est à dire catégoriquement un morphisme de l’objet terminal de la tribu vers l’objet E

Page 22 sur 81

A est un objet d’une tribu C c’est à dire un type

On considère le foncteur changement de base ( foncteur de substitution) le long du morphisme unique de A vers l’objet terminal de la tribu :

A → *

iA : C → C(A)

C’est un homomorphisme de tribus ( voir Page 21 sur 81)

Par définition : iA( E)= ( ExA, p2)

(Voir Page 12 sur 81)

Ce foncteur correspond en théorie des types à une régle de déduction appelée affaiblissement contextuel , qui consiste à déduire :

x:A ⊢E: Type

De

E: Type

Page 23 sur 81 un rappel d’algèbre : étant donné un anneau commutatif R, on peut envisager l’extension polynomiale:

i : R → R[x]

qui est engendré de manière libre (freely) par l’élément x qui est générique, pouvant prendre n’importe quelle valeur

https://fr.m.wikipedia.org/wiki/Anneau_(mathématiques)

https://fr.m.wikipedia.org/wiki/Anneau_commutatif

Le caractère libre de l’extension est représenté page 23 sur 81 par un diagramme commutatif triangulaire :

Pour tout homéomorphisme d’anneaux h : R → S et tout élément s de S, il existe un homomorphisme h unique (propriété universelle):

h : R[x] → S

Avec hi = f et h(x)= s

La page suivante 24 sur 81 « Generic terms «  réalise l’analogie de cette notion algébrique d’extension libre avec la situation catégorique ici.

L’analogue de l’homomorphisme d’anneaux i page 23 est le foncteur :

i : C → C(A)

qui envoie l’objet A de C sur l’objet de C(A) (A x A, p2) =i(A)

Le morphisme diagonal dans C :

δA : A → A x A

Est aussi un morphisme dans C(A)

δA : * → i(A)

i(A) qui est , comme objet de C(A) , un type, dont δA est un terme

δA : i(A)

C’est un terme générique qui réalise l’analogie avec le terme générique x de la page 23 précédente

On peut donc dire (théorème page 24 sur 81) que l’extension

i : C → C(A)

est librement engendrée par le terme δA: i(A) qui est un terme générique

Et l’on note C(A)= C[x] avec x= δA

Les termes génériques apparaissent aussi dans cet exposé d’André Joyal:

http://home.sandiego.edu/~shulman/cmshighercategories2013/Joyal.pdf

Pages 21 et 22 sur 75 titrées « Generic terms »

Le foncteur changement de base

i : C → C(A)

est un foncteur logique (voir Page 19 sur 75 la page 20 donne des exemples de foncteurs logiques dont le foncteur de Yoneda, le foncteur changement de base le long d’un morphisme quelconque f : A → B )

Un foncteur entre des catégories localement cartésiennes fermées (lccc = locally cartesian closed) est dit logique s’il préserve les limites finies et les produits internes.

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