Hirschowitz, André ;
Hirschowitz, Tom ;
Tabareau, Nicolas
Wild omegaCategories for the Homotopy Hypothesis in Type Theory
Abstract
In classical homotopy theory, the homotopy hypothesis asserts that the fundamental varpigroupoid construction induces an equivalence between topological spaces and weak varpigroupoids. In the light of Voevodsky's univalent foundations program, which puts forward an interpretation of types as topological spaces, we consider the question of transposing the homotopy hypothesis to type theory. Indeed such a transposition could stand as a new approach to specifying higher inductive types. Since the formalisation of general weak varpigroupoids in type theory is a difficult task, we only take a first step towards this goal, which consists in exploring a shortcut through strict varpicategories.
The first outcome is a satisfactory typetheoretic notion of strict varpicategory, which has hsets of cells in all dimensions. For this notion, defining the 'fundamental strict varpicategory' of a type seems out of reach. The second outcome is an 'incoherently strict' notion of typetheoretic varpicategory, which admits arbitrary types of cells in all dimensions. These are the 'wild' varpicategories of the title. They allow the definition of a 'fundamental wild varpicategory' map, which leads to our (partial) homotopy hypothesis for type theory (stating an adjunction, not an equivalence).
All of our results have been formalised in the Coq proof assistant. Our formalisation makes systematic use of the machinery of coinductive types.
BibTeX  Entry
@InProceedings{hirschowitz_et_al:LIPIcs:2015:5166,
author = {Andr{\'e} Hirschowitz and Tom Hirschowitz and Nicolas Tabareau},
title = {{Wild omegaCategories for the Homotopy Hypothesis in Type Theory}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {226240},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897873},
ISSN = {18688969},
year = {2015},
volume = {38},
editor = {Thorsten Altenkirch},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5166},
URN = {urn:nbn:de:0030drops51669},
doi = {10.4230/LIPIcs.TLCA.2015.226},
annote = {Keywords: Homotopy Type theory; Omegacategories; Coinduction; Homotopy hypothesis}
}
2015
Keywords: 

Homotopy Type theory; Omegacategories; Coinduction; Homotopy hypothesis 
Seminar: 

13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Issue date: 

2015 
Date of publication: 

2015 