Category Archives: ∞-topoi

(∞,1)-catégories internes

https://ncatlab.org/nlab/show/category+object+in+an+%28infinity%2C1%29-category Une catégorie interne dans une (∞, 1)-catégorie C est un objet simplicial dans C: https://ncatlab.org/nlab/show/simplicial+object+in+an+%28infinity%2C1%29-category c’est à dire un (∞, 1)-foncteur : https://ncatlab.org/nlab/show/%28infinity%2C1%29-functor Une catégorie double (“double category”) est une catégorie interne à Cat (catégorie de toutes les catégories): … Continue reading

Posted in ∞-catégories, ∞-topoi, category theory, Higher category theory, Higher topos theory | Leave a comment

#ScienceInternelle #Chuspaces un cadre mathématique pour la dualité cartésienne corps-esprit

J’ai déjà parlé ici des espaces et catégories de Chu : https://anthroposophiephilosophieetscience.wordpress.com/2017/03/05/scienceinternelle-15-chuspaces-les-espaces-de-chu/ et de cet article philosophique de Vaughan Pratt: http://boole.stanford.edu/pub/ratmech.pdf Depuis la découverte de la théorie homotopique des types (HoTT, ou homotopy type theory) vers 2006, tout le monde … Continue reading

Posted in ∞-catégories, ∞-topoi, Chu spaces, Descartes, homotopy type theory, Philosophie, Science-internelle | Tagged , , | Leave a comment

Simplicial objects in infinity-categories

Originally posted on Climbing Mount Bourbaki:
Let be an -category, in the sense of Joyal and Lurie: in other words, a quasicategory or weak Kan complex. For instance, for the purposes of Hopkins-Miller, we’re going to be interested in the…

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

#HoTT : The Book : 1.4 dependent function types (Π-types)

Les éléments d’un Π-type sont des fonctions dont le codomaine (la cible) qui est un type varie avec l’élément du domaine A (un autre type) auquel la fonction s’applique; ce sont des fonctions dirigées de À vers l’univers U dont … Continue reading

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

Categorical models of dependent types

Cette page : https://ncatlab.org/nlab/show/categorical+model+of+dependent+types Définit des notions que nous avons déjà rencontrées, comme “display maps” , “comprehension categories”, fibrations… Elle aide ainsi à comprendre, comme les notes de Joyal ou de Shulman, les correspondances entre théorie des catégories et HoTT … Continue reading

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

Correspondance entre théorie des catégories et #HoTT : deux autres exposés

Un autre exposé de Joyal sur categorical #HoTT , différant sensiblement de celui déjà étudié: http://www.math.uwaterloo.ca/~asl2013/Slides/Joyal.pdf Un exposé de Michael Shulman sur les “categorical models ” de HoTT: https://home.sandiego.edu/~shulman/hottminicourse2012/03models.pdf revenant sur la notion de “display map”, aussi expliquée par Joyal … Continue reading

Posted in ∞-catégories, ∞-topoi, category theory, Higher category theory, Higher topos theory, homotopy type theory, Philosophie mathématique | Tagged , | Leave a comment

André Joyal : categorical #HoTT 3

Nous poursuivons l’étude de la précieuse conférence de Joyal qui est ici : https://ncatlab.org/homotopytypetheory/files/Joyal.pdf Il est tout à fait utile d’étudier ce texte en même temps que le Big Book de HoTT pour garder le parallèle des notions catégoriques ( … Continue reading

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