An Interesting Link Between Type Theory and Algebraic topology.

François Lamarche 1, *
* Auteur correspondant
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Henri Poincaré invented both homology and homotopy theory around 1899. The spaces he used for homotopy were pieces of R^n glued together; the general concept of topological spaces had not been invented yet. He could not do the same for homology, so he resorted to simple combinatorial objects to define the necessary spaces, which he called simplicial complexes, and where computations were easy anyway. It is only in the forties that Eilenberg showed how do define homology directly on topological spaces, and in the early fifties that combinato- rial objects were found--that we now call simplicial sets, and that are also due to Eilenberg and his students--which are sufficiently powerful to enable direct definitions and quite a few computations in homotopy. The most fundamental concept of homotopy is the notion of path between two points in a space. For several years it has been tempting to give a logical meaning to this notion of path, namely as "a constructive proof that two points are equal". One way to formalize this intuitive notion would be to interpret the Martin-Lo ̈f type-theoretical equality predicate in a suitable category of spaces. The first positive results in this direction have been given by Michael Warren, working under the supervision of Steve Awodey. They are quite technical and depend very much on modern abstract homotopy theory à la Quillen. I will present a very concrete model, which I also think is the simplest that has been discovered so far. It is based on a well-known specialization of simplicial set, for which I will define a concrete path object which doubles as an identity type, along with a suitable notion of dependent type.
Type de document :
Communication dans un congrès
SD09 Structures and Deductions 2009, Jul 2009, Bordeaux, France. 2009
Liste complète des métadonnées
Contributeur : Francois Lamarche <>
Soumis le : mercredi 7 septembre 2011 - 13:45:14
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48


  • HAL Id : inria-00620172, version 1



François Lamarche. An Interesting Link Between Type Theory and Algebraic topology.. SD09 Structures and Deductions 2009, Jul 2009, Bordeaux, France. 2009. 〈inria-00620172〉



Consultations de la notice