#HoTT : André Joyal retour sur les règles de formation, d’introduction, d’élimination et de calcul

Ces notes d’andré Joyal :

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

Reviennent sur ces règles, en pages 10 à 12 sur 39

Ces règles très importantes et qui reviennent à tout bout de champ sont expliquées dans The Book :

The HoTT Book

Page 27 , au paragraphe 1.5 « product types » , voir aussi cet article :

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/27/hott-the-book-product-types-dependent-pair-types-ou-σ-type/

« 1 règles de formation, expliquant comment former ce nouveau genre de types

Exemple : si A, B sont des types, on peut former le type des fonctions :

A → B
2 “constructeurs” (constructor “), règles d’introduction : comment former les éléments de ce nouveau type

Exemple : une seule règle pour les types de fonction, la λ-abstraction

3 les “éliminateurs” ou règles d’élimination, expliquant comment utiliser les éléments de ce nouveau type Exemple : le type des fonctions a une seule régle d’élimination, l’application d’une fonction.

4 les règles de calcul (computation rules) :comment un éliminateur agit sur un constructeur. Exemple : pour les types de fonction, (λx.Φ)( a) est égale par jugement (non définitionnellement ) à l’expression de Φ où l’on substitue a à x

5 un principe d’unicité (éventuel) pour un type, portant sur l’unicité des flèches (maps) en direction ou venant de ce type. »

La règle de formation pour les sommes est expliquée page 10 ( de la note indiquée en début de cet article)ce qui est en dessous de la barre est dédut de ce qui est au dessus, qui constitue les prémisses, ainsi de :

x:A ⊢ E(x): Type

Qui asserte que pour x variant dans A , si E(x) est un type, on déduit l’existence d’un nouveau type somme (un type dépendant) :

x:A E(x)

La règle d’introduction est expliquée page 10 pour les paires (a,b); des prémisses que sont les jugements (au dessus de la barre):

⊢a:A

⊢b: E(a)

On déduit :

⊢ (a,b):∑x:AE(x)

La régle de formation des produits est abordée Page 11 sur 39

du jugement :

⊢E(x): Type

Dans le contexte x:A ( x est un terme du Type A)

On déduit (règle de formation d’un nouveau type)le jugement qui forme un nouveau type Produit indexé par x terme variable de A

⊢ Πx:AE(x)

S’ensuit sur la même page une règle d’introduction des éléments de ce nouveau type

Du jugement ⊢t:E(x) dans le contexte x:A , jugement qui asserte que si x est un terme de A, t (qui dépend de x t= t(x)) est un terme de E(x), on déduit le jugement assertant que le λ- terme correspondant est un terme du nouveau type Produit :

⊢λx.t : Πx:AE(x)

où λx.t(x) désigne la fonction qui associe à x le terme t(x) de E(x)
S’ensuit une régle d’élimination (un éliminateur ) expliquant comment utiliser ces termes du nouveau type, construits en accord avec la régle d’introduction précédente (appelée aussi un Constructeur):
Des jugements :

⊢a:A et ⊢ f:Πx:A on déduit :

⊢f(a):E(a)

La règle d’élimination nous dit comment utiliser les termes construits par le constructeur (ou règle d’introduction), termes du nouveau type bâti selon la règle de formation.

Page 12 sur 39, est expliquée la règle de calcul (computation rule) ou comment l’éliminateur agit sur le constructeur:

De ⊢a:A et ⊢λx.t(x):Πx:AE(x)

on déduit l’égalité (non définitionnelle)( en remplaçant x par a dans l’expression qui est sous la juridiction du λ)

⊢(λx.t(x))(a) ≡t(a)

Enfin, toujours page 12, le principe d’unicité des fonctions sortant ou allant vers le nouveau type (ici le produit) (uniqueness rule )

De ⊢f:Πx:AE(x)

On déduit :

⊢f≡λx.f(x)

Les règles de formation , d’introduction , d’élimination et de calcul des produits sont aussi abordées aux pages 31, 32 de ce cours :

https://synapse.math.univ-toulouse.fr/s/QWrxKeXn31mN3gz/download?path=%2F&files=Joyal_Theory%20of%20tribes%202.pdf

Pour récapituler, quatre règles :

De formation (pour former de nouveaux types à partir des anciens ) , d’introduction (ou constructeur, comment construire les termes de ce nouveau type) , d’élimination ( comment utiliser ces termes ) et de calcul ( computation , spécifiant comment un éliminateur agit sur un constructeur) plus un principe d’unicité des fonctions allant vers ou venant des nouveaux types formés selon les règles de formation

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