eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-08-30
28:1
28:16
10.4230/LIPIcs.FSCD.2017.28
article
Models of Type Theory Based on Moore Paths
Orton, Ian
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 on cubical sets, the notion of model presented here is notable for avoiding any form of Kan filling condition in the semantics of types.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol084-fscd2017/LIPIcs.FSCD.2017.28/LIPIcs.FSCD.2017.28.pdf
dependent type theory
homotopy theory
Moore path
topos