An Interesting Link Between Type Theory and Algebraic topology.

International audienceHenri 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