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

François Lamarche 1
1 SEMAGRAMME - Semantic Analysis of Natural Language
Inria Nancy - Grand Est, LORIA - NLPKD - Department of Natural Language Processing & Knowledge Discovery
Abstract : 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-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.
Liste complète des métadonnées

Contributor : Francois Lamarche <>
Submitted on : Friday, September 23, 2011 - 9:16:35 AM
Last modification on : Tuesday, December 18, 2018 - 4:38:01 PM


  • HAL Id : inria-00625956, version 1



François Lamarche. A new homotopy-theoretic interpretation of Martin-Löf's identity type.. Models, Logics and Higher-Dimensional Categories: A Tribute to the Work of Mihaly Makkai, Bradd Hart and Thomas G. Kucera and Anand Pillay and Philip J. Scott and Robert A. G. Seely, Jun 2011, Montréal, Canada. ⟨inria-00625956⟩



Record views