License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2016.24
URN: urn:nbn:de:0030-drops-65647
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6564/
Go to the corresponding LIPIcs Volume Portal

Orton, Ian ; Pitts, Andrew M.

Axioms for Modelling Cubical Type Theory in a Topos

pdf-format:
LIPIcs-CSL-2016-24.pdf (0.6 MB)

Abstract

The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an interval-like object I in a topos to give a model of type theory in which elements of identity types are functions with domain I. Cohen, Coquand, Huber and Mörtberg give such a model using a particular category of presheaves. We investigate the extent to which their model construction can be expressed in the internal type theory of any topos and identify a collection of quite weak axioms for this purpose. This clarifies the definition and properties of the notion of uniform Kan filling that lies at the heart of their constructive interpretation of Voevodsky's univalence axiom. Furthermore, since our axioms can be satisfied in a number of different ways, we show that there is a range of topos-theoretic models of homotopy type theory in this style.

BibTeX - Entry

@InProceedings{orton_et_al:LIPIcs:2016:6564,
  author =	{Ian Orton and Andrew M. Pitts},
  title =	{{Axioms for Modelling Cubical Type Theory in a Topos}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{24:1--24:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Jean-Marc Talbot and Laurent Regnier},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6564},
  URN =		{urn:nbn:de:0030-drops-65647},
  doi =		{10.4230/LIPIcs.CSL.2016.24},
  annote =	{Keywords: models of dependent type theory, homotopy type theory, cubical sets, cubical type theory, topos, univalence}
}

Keywords: models of dependent type theory, homotopy type theory, cubical sets, cubical type theory, topos, univalence
Collection: 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
Issue Date: 2016
Date of publication: 29.08.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI