Daily Archives: October 14, 2017

Homotopy Theory in Type Theory: Progress Report

Originally posted on Homotopy Type Theory:
A little while ago, we gave an overview of the kinds of results in homotopy theory that we might try to prove in homotopy type theory (such as calculating homotopy groups of spheres), and the basic…

Posted in Philosophie

Voir l’Univers dans un topos

https://ncatlab.org/nlab/show/universe+in+a+topos et cet article de Streicher : Click to access UniTop.pdf William Blake : voir un Univers dans un grain de sable et le ciel dans une fleur des champs http://poemescitations.over-blog.com/william-blake-univers.html http://www.apophtegme.com/SPICILEGE/LITTERATURE/blake.htm

Posted in ∞-catégories, ∞-topoi, category theory, Higher category theory, Higher topos theory, homotopy type theory, Littérature-Poésie, Philosophie, Philosophie mathématique, Science, mathesis, Science-internelle | Tagged ,

Path categories and propositional identity types

Originally posted on Henosophia TOPOSOPHIA μαθεσις uni√ersalis τοποσοφια MATHESIS οντοποσοφια ενοσοφια:
Source?: Path categories and propositional identity types

Posted in Philosophie

Kapulkin : locally cartesian closed quasicategories from type theory

Originally posted on HENOSOPHIA τοποσοφια μαθεσις υνι√ερσαλις οντοποσοφια:
http://www-home.math.uwo.ca/~kkapulki/papers/qcats-from-type-theory.pdf

Posted in Philosophie

Kapulkin : Joyal’s conjecture in #HoTT

Click to access Kapulkin-dissertation.pdf

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

Awodey : natural models of #HoTT

Click to access natural.pdf

Posted in Philosophie | Tagged

A category – theoretic version of the identity type weak factorization system

Click to access 1412.0153.pdf Cet article aborde plusieurs des notions d’André Joyal, en relation avec la théorie des types, notamment celle de tribu , une sorte particulière de catégorie, je suis de plus en plus convaincu que c’est là qu’il … Continue reading

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

Lettre d’André Joyal à Grothendieck

Click to access lettreJoyal.pdf

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

Sept textes d’André Joyal

http://www.iecl.univ-lorraine.fr/~Pierre-Yves.Gaillard/DIVERS/Joyal/

Posted in category theory, Higher category theory, Higher topos theory, Philosophie, Philosophie mathématique, Science, mathesis, Science-internelle | Tagged

André Joyal #HoTT : tribus et ⊓-tribus

Les articles d’andré Joyal, comme ceux de Mike Shulman, apportent l’intelligibilité de la théorie des catégories à la théorie homotopique des types, et renforcent le lien entre les deux domaines: Click to access Joyal.pdf Le livre de Quillen « Homotopical algebra » … Continue reading

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