Category Archives: homotopy type theory

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 The Book : 1.11 propositions as types

The HoTT Book https://hott.github.io/book/nightly/hott-online-1075-g3c53219.pdf Je passe sur ce qui n’est pas essentiel pour aller plus vite car il faut accélérer pour en arriver aux choses sérieuses qui commencent au chapitre 2. Passons donc Page 41 au 1.11: Les termes ou … Continue reading

Posted in homotopy type theory | Leave a comment

Fibration categories and Type theory

http://www.lorentzcenter.nl/lc/web/2011/467/presentations/Presentation%20C%20Kapulkin.pdf

Posted in Homotopy, homotopy type theory | Leave a comment

Categories types and structures

https://www.di.ens.fr/users/longo/files/CategTypesStructures/book.pdf

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

#HoTT André Joyal : la notion de typos

Voir cet ancien article : https://anthroposophiephilosophieetscience.wordpress.com/2017/10/14/andre-joyal-hott-tribus-et-⊓-tribus/ et la note de Joyal : http://www.math.uwaterloo.ca/~asl2013/Slides/Joyal.pdf Page 15 sur 52 définition du «  push forward functor » associé à une flèche f : A → B dans une catégorie C Le foncteur est noté … Continue reading

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

#HoTT : Voevodsky (2009) notes on Type systems

https://pdfs.semanticscholar.org/4bc5/ab7b810f2b10d04e186667b4647b741a8419.pdf?_ga=2.23829306.1211623468.1508579635-742940545.1491914182 De Voevodsky aussi : Homotopy type systems https://ncatlab.org/homotopytypetheory/files/HTS.pdf

Posted in Homotopy, homotopy type theory | Leave a comment

#HoTT : André Joyal weak factorisation system

Deux liens sur les deux wikis de la théorie des catégories: https://ncatlab.org/joyalscatlab/published/Weak+factorisation+systems https://ncatlab.org/nlab/show/weak+factorization+system André Joyal explique aussi la notion dans ses notes, par exemple Page 34 et 35 de : http://www.math.uwaterloo.ca/~asl2013/Slides/Joyal.pdf qui a été étudiée ici : https://anthroposophiephilosophieetscience.wordpress.com/2017/10/14/andre-joyal-hott-tribus-et-⊓-tribus/ Page 34 … Continue reading

Posted in ∞-catégories, ∞-topoi, category theory, Higher category theory, homotopy type theory, Philosophie mathématique, Science-internelle, Théorie des topoi (topos theory) | Tagged , , | Leave a comment