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.FSCD.2017.28
URN: urn:nbn:de:0030-drops-77149
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7714/
Go to the corresponding LIPIcs Volume Portal

Orton, Ian ; Pitts, Andrew M.

Models of Type Theory Based on Moore Paths

pdf-format:
LIPIcs-FSCD-2017-28.pdf (0.6 MB)

Abstract

This paper introduces a new family of models of intensional Martin-Löf type theory. We use constructive ordered algebra in toposes. Identity types in the models are given by a notion of Moore path. By considering a particular gros topos, we show that there is such a model that is non-truncated, i.e. contains non-trivial structure at all dimensions. In other words, in this model a type in a nested sequence of identity types can contain more than one element, no matter how great the degree of nesting. Although inspired by existing non-truncated models of type theory based on simplicial and on cubical sets, the notion of model presented here is notable for avoiding any form of Kan filling condition in the semantics of types.

BibTeX - Entry

@InProceedings{orton_et_al:LIPIcs:2017:7714,
  author =	{Ian Orton and Andrew M. Pitts},
  title =	{{Models of Type Theory Based on Moore Paths}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{28:1--28:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Dale Miller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7714},
  URN =		{urn:nbn:de:0030-drops-77149},
  doi =		{10.4230/LIPIcs.FSCD.2017.28},
  annote =	{Keywords: dependent type theory, homotopy theory, Moore path, topos}
}

Keywords: dependent type theory, homotopy theory, Moore path, topos
Collection: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Issue Date: 2017
Date of publication: 30.08.2017

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