Orton, Ian and Pitts, Andrew M. - Models of Type Theory Based on Moore Paths

lmcs:4292 - Logical Methods in Computer Science, January 9, 2019, Volume 15, Issue 1
Models of Type Theory Based on Moore Paths

Authors: Orton, Ian and Pitts, Andrew M.

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 cubical sets, the notion of model presented here is notable for avoiding any form of Kan filling condition in the semantics of types.


Source : oai:arXiv.org:1802.05629
DOI : 10.23638/LMCS-15(1:2)2019
Volume: Volume 15, Issue 1
Section: Type theory and constructive mathematics
Published on: January 9, 2019
Submitted on: February 16, 2018
Keywords: Computer Science - Logic in Computer Science,F.4.1,F.3.2


Share