Models of Type Theory Based on Moore Paths
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.