Tag Archives: HoTT

Type-theoretic model category

https://ncatlab.org/nlab/show/type-theoretic+model+category Page citée sur celle ci : https://ncatlab.org/nlab/show/identity+type

Posted in category theory, Higher category theory, homotopy type theory | Tagged

#HoTT : le cours d’André Joyal en cinq parties sur les tribus

Partie 1: Click to access download Partie 2: Click to access download Partie 3: Click to access download Partie 4: Click to access download Partie 5: Click to access download

Posted in ∞-catégories, category theory, homotopy type theory | Tagged , , ,

Bolzano : une théorie des idées

J’avais acheté la récente édition à « Oxford logic guides «  de « bolzano’s Logical system « : https://anthroposophiephilosophieetscience.wordpress.com/2016/11/06/de-bolzano-aux-recherches-logiques-de-husserl/ https://themasters6.wordpress.com/2016/11/06/bolzanos-logical-system/ Or il s’avère que Bolzano décrit un système formel et une théorie d’idées , qui sont les objets de base de ses travaux, … Continue reading

Posted in homotopy type theory, Logique, Philosophie | Tagged , , ,

Church : a formulation of The simple theory of types

Click to access church-1940.pdf Cité par Joyal dans: Click to access Joyal.pdf Voir aussi: https://plato.stanford.edu/entries/type-theory-church/ Click to access andrewsfest12.pdf

Posted in homotopy type theory, Logique, Philosophie | Tagged ,

T Streicher : a model of type theory in simplicial sets – a brief introduction to Voevodsky’s #HoTT

https://ncatlab.org/nlab/show/T.+Streicher+-+a+model+of+type+theory+in+simplicial+sets+-+a+brief+introduction+to+Voevodsky%27+s+homotopy+type+theory L’article de T Streicher se lit en cliquant sur la référence au début. Comme on l’a vu dans l’article 15 récent du Hashtag #HigherToposTheory, les ensembles simpliciaux , qui sont des foncteurs ayant pour cible Set, s’organisent en une … Continue reading

Posted in ∞-catégories, ∞-topoi, category theory, Higher category theory, Higher topos theory, homotopy type theory, Philosophie, Théorie des topoi (topos theory) | Tagged , , ,

Awodey : cubical #HoTT 1

Click to access slides_awodey.pdf Il n’est pas question ici de se lancer dans les arcanes des “cubical sets” et des recherches récentes sur la “cubical HoTT”, à la fin de cette note, mais de comparer les pages du début à … Continue reading

Posted in homotopy type theory | Tagged , ,

La théorie des types et ses applications à la Science des ordinateurs

Click to access cb79306cd0d1e5870b5f0b8038c3c94983fd.pdf La théorie des types émerge des travaux de Bertrand Russell , au début du 20eme siècle, elle atteint des niveaux plus sophistiqués dans les recherches de logiciens comme Alonso Chirch , HoTT en est le stade … Continue reading

Posted in ∞-catégories, ∞-topoi, Homotopy, homotopy type theory | Tagged , ,

#HoTT : une nouvelle fondation pour les mathématiques du 21eme siècle

http://aperiodical.com/2013/06/homotopy-type-theory-a-new-foundation-for-21st-century-mathematics/

Posted in homotopy type theory | Tagged

Joyal : categorical #HoTT 1

Click to access Joyal.pdf La définition importante (Page 13-14 sur 81) est celle de tribu (“tribe “) , c’est à dire une catégorie C munie d’une structur de tribu F (une sous-catégorie F de C) et d’un objet terminal. Les … Continue reading

Posted in category theory, homotopy type theory | Tagged ,

Andrei Rodin : Logic and geometry in topos theory and #HoTT 1

Ce travail d’Andrei Rodin: Click to access am2.pdf fait suite, ou accompagne, cet autre que nous avons étudié ici: Click to access RODIN_Andrei.pdf Le domaine de prédilection de ce philosophe est la méthode axiomatique: https://arxiv.org/abs/1210.1478 Page 3: La “received axiomatic … Continue reading

Posted in ∞-catégories, ∞-topoi, category theory, Higher category theory, Homotopy, homotopy type theory, Philosophie, Philosophie mathématique, Science, mathesis, Science-internelle | Tagged , , , ,