#HoTT : The Book : 1.4 dependent function types (Π-types)

Les éléments d’un Π-type sont des fonctions dont le codomaine (la cible) qui est un type varie avec l’élément du domaine A (un autre type) auquel la fonction s’applique; ce sont des fonctions dirigées de À vers l’univers U dont les types sont éléments:

A → U

Qui sont notées de façon équivalente :

Πx:A B(x)

ou

Π(x:A), B(x)

Si B est une famille constante, on retrouve la notion classique de “function type”:

Πx:A B(x) ≡ A → B

Fonctions polymorphiques

Ce sont des fonctions qui ont pour argument un type et agissent sur un élément de ce type ou d’autres types construits à partir de lui. Un exemple est la fonction polymorphique identité :

ΠA(U) → A

Définie par λ-abstraction :

Id:≡λ(A: U).λ(x:A).x

La λ-abstraction est définie quelques pages avant , Page 22

Ainsi g(x, _) est la même chose que λy.g(x,y)

Par convention la plus grande force liante est celle d’une expression où intervient λ, ainsi λx. S’applique à la totalité de ce qui est écrit après , seule un parenthésage permet de stopper cette force liante, par exemple

λX.x+x équivaut à λx.(x+x)

Pour toute fonction f : A → B

On peut former par λ-abstraction:

λx.f(x) qui est égale par définition à f :

f≡λx.f(x)

C’est le principe : une fonction est uniquement déterminée par ses valeurs

On a, par définition :

(λx.Φ)(a)≡Φ’

Où Φ’ est l’expression Φ où l’on remplace systématiquement x par a, par exemple :

(λx.x+x) (2)≡ 2+2

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