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 Advertisements

Posted in category theory, Higher category theory, homotopy type theory | Tagged | Leave a comment

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

Partie 1: https://synapse.math.univ-toulouse.fr/s/QWrxKeXn31mN3gz/download?path=%2F&files=Joyal_Theory%20of%20tribes%201.pdf Partie 2: https://synapse.math.univ-toulouse.fr/s/QWrxKeXn31mN3gz/download?path=%2F&files=Joyal_Theory%20of%20tribes%202.pdf Partie 3: https://synapse.math.univ-toulouse.fr/s/QWrxKeXn31mN3gz/download?path=%2F&files=Joyal_Theory%20of%20tribes%203.pdf Partie 4: https://synapse.math.univ-toulouse.fr/s/QWrxKeXn31mN3gz/download?path=%2F&files=Joyal_Theory%20of%20tribes%204.pdf Partie 5: https://synapse.math.univ-toulouse.fr/s/QWrxKeXn31mN3gz/download?path=%2F&files=Joyal_Theory%20of%20tribes%205.pdf

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

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

https://www.classes.cs.uchicago.edu/archive/2007/spring/32001-1/papers/church-1940.pdf Cité par Joyal dans: https://ncatlab.org/homotopytypetheory/files/Joyal.pdf Voir aussi: https://plato.stanford.edu/entries/type-theory-church/ https://www.cs.cmu.edu/~fp/talks/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

http://www.helsinki.fi/lc2015/materials/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 à celles du travail … Continue reading

Posted in homotopy type theory | Tagged , ,

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

https://pdfs.semanticscholar.org/7f8b/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 le plus moderne … Continue reading

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