References & Citations
Computer Science > Logic in Computer Science
Title: Models of Type Theory Based on Moore Paths
(Submitted on 15 Feb 2018 (v1), last revised 8 Jan 2019 (this version, v3))
Abstract: This paper introduces a new family of models of intensional Martin-L\"of 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.
Submission history
From: Thorsten Wissmann [view email] [via LOGICAL proxy][v1] Thu, 15 Feb 2018 16:01:02 GMT (29kb)
[v2] Fri, 28 Dec 2018 19:59:31 GMT (31kb)
[v3] Tue, 8 Jan 2019 15:27:10 GMT (39kb,D)
Link back to: arXiv, form interface, contact.