A new homotopy-theoretic interpretation of Martin-Löf's identity type.

International audienceThe 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-Lö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 the well-known fact that the category of categories can be embedded in the category of simplicial sets, the workhorse of homotopy theory since the fifties. I will show how to interpret dependent types therein, and I will define several concrete path object functors, which can be used to interpret identity types. Moreover they can be used to give a simple and concrete definition of homotopy for categories