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.
Type de document :
Communication dans un congrès
Models, Logics and Higher-Dimensional Categories: A Tribute to the Work of Mihaly Makkai, Jun 2011, Montréal, Canada. 53, 2011, CRM Proceedings & Lecture Notes
Liste complète des métadonnées

https://hal.inria.fr/inria-00625956
Contributeur : Francois Lamarche <>
Soumis le : vendredi 23 septembre 2011 - 09:16:35
Dernière modification le : jeudi 11 janvier 2018 - 06:23:32

Identifiants

  • HAL Id : inria-00625956, version 1

Collections

Citation

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, Jun 2011, Montréal, Canada. 53, 2011, CRM Proceedings & Lecture Notes. 〈inria-00625956〉

Partager

Métriques

Consultations de la notice

109