#HoTT The Book : type 2 of booleans; type N of natural numbers

The HoTT Book

L’ensemble 2={0, 11} des deux valeurs de vérité Vrai (1) et Faux (0) est un type à deux termes ; 2: U que l’on retrouve souvent en programmation :

https://en.m.wikipedia.org/wiki/Boolean_data_type

Il peut être construit comme coproduit (Somme) à partir du type unité 1 par :

2= 1+1

Cependant on peut aussi procéder en sens inverse et dériver les coproduits à partir de 2 et des ∑-types.

Les Σ-types pouvant être consiérés comme des unions disjointes indexées et un coproduit étant une union disjointe binaire, il est naturel d’attendre qu’une somme A+B soit indexée sur le type 2 à deux éléments d’où la formule page 36

Le récurseur correspond à la boucle If-then- else en programmation

En 1.9 Page 36 on aborde le plus simple type infini auquel l’on puisse penser, celui des entiers naturels. Les éléments sont construits récursivement , à partir de 0: N et de la fonction successeur :

Succ : N → N

Ainsi 1 ≡ succ (0) etc…

La propriété fondamentale des entiers est que l’on peut définir des fonctions par récursion et formaliser des démonstrations par récurrence .

Advertisements
This entry was posted in homotopy type theory. Bookmark the permalink.