Hiérarchie d’univers ; l’univers d’ordre n n’est pas un n-type

https://pdfs.semanticscholar.org/dbba/a6c2e087836ecda1d39a8955e75a3cb23253.pdf

https://arxiv.org/pdf/1311.4002.pdf

Un type est élément d’un univers

Étant donné un entier n supérieur ou égal à -2 , un type A est dit être un n-type, ou n-tronqué (n-truncated) ou de h-niveau ( h-level) n+2 si le type Is-n-Type (A) est habité

Voir Page 3 du lien Arxiv ci dessus

Un type -2-tronqué (de h-niveau 0)est dit contractible:

https://ncatlab.org/nlab/show/contractible+type

Un -1-type est une proposition; un 0-type est un ensemble.

http://www.cs.nott.ac.uk/~psznk/docs/thesisagda_nicolai/HHHUU-ComplicatedTypes.html

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