Daily Archives: January 4, 2018

L’article très important de Kapulkin et Szumilo dont parle André Joyal

C’est dans une de ses notes sur les tribus (« categorical homotopy type theory ») que Joyal parle de ce résultat: http://logica.dmi.unisa.it/tacl/wp-content/uploads/abstracts/invited_paper_7.pdf qui est démontré ici: https://arxiv.org/abs/1709.09519 Équivalence de la théorie de l’homotopie des tribus de Joyal et de celle des « fibration … Continue reading

Posted in homotopy type theory | Tagged , ,

Lumsdaine, Warren : local universes model

Originally posted on Henosophia TOPOSOPHIA μαθεσις uni√ersalis τοποσοφια MATHESIS οντοποσοφια ενοσοφια Philosophie, théorie des catégories et théorie homotopique des types:
https://arxiv.org/abs/1411.1736

Posted in Philosophie

Google Plus : David Roberts sur les travaux d’André Joyal #HoTT

https://plus.google.com/+DavidRoberts/posts/QqpHm3BxsM7 On y trouve les « Notes on clans and tribes » sur Arxiv https://anthroposophiephilosophieetscience.wordpress.com/2017/10/28/hott-andre-joyal-tribus-et-clans/ ainsi que ce lien sur Nlab: https://ncatlab.org/nlab/show/categorical+model+of+dependent+types#Joyal17 Toute la collection de David Roberts est intéressante: https://plus.google.com/collection/0GL2Y On y trouve notamment pour les UF de Voevodsky: https://arxiv.org/abs/1711.01477

Posted in category theory, Higher category theory, homotopy type theory, Philosophie mathématique, Science, mathesis, Science-internelle

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 … Continue reading

Posted in homotopy type theory

Pi et Sigma types

http://www.cs.nott.ac.uk/~psztxa/ntt/pisigma.pdf

Posted in Computer science, homotopy type theory

#HoTT The Book : sets, Logic and types

The HoTT Book Chapitre 3 page 107 https://www.andrew.cmu.edu/user/awodey/preprints/stcsFinal.pdf http://publish.uwo.ca/~jbell/types.pdf Nous voyons avec ce triplet « types, sets, categories » que la théorie des types s’insère entre les ensembles et les catégories soit deux systèmes d’Idées qui jouent ici le rôle de représentants … Continue reading

Posted in homotopy type theory, Philosophie