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 on cubical sets, the notion of model presented here is notable for avoiding any form of Kan filling condition in the semantics of types.
Although our use of constructive algebra within toposes to make models of intensional type theory appears to be new, we are not the only ones to consider using some form of path with strictly unitary and associative composition to model identity types with a judgemental computation rule. Van den Berg and Garner @cite_7 use topological Moore paths and a simplicial version of them to get instances of their notion of for modelling identity types. The results of Sections and show that any ordered abelian group in a topos induces a path object category structure on that topos; and since the notion of fibration we use (Definition ) is closely related to the one used in @cite_7 (see Proposition 6.1.5 of that paper), one can get alternative, more abstract categorical proofs of Theorems and from the work of Van den Berg and Garner. However, the concrete calculations in the internal language that we give are quite simple by comparison; and this approach proves its worth in , whose results on obtaining function extensionality from the ordered ring structure are new.
@cite_7
1997582403
In this paper we construct new categorical models for the identity types of Martin-Lof type theory, in the categories Top of topological spaces and SSet of simplicial sets. We do so building on earlier work of Awodey and Warren [2009], which has suggested that a suitable environment for the interpretation of identity types should be a category equipped with a weak factorization system in the sense of Bousfield--Quillen. It turns out that this is not quite enough for a sound model, due to some subtle coherence issues concerned with stability under substitution; and so our first task is to introduce a slightly richer structure, which we call a homotopy-theoretic model of identity types, and to prove that this is sufficient for a sound interpretation. Now, although both Top and SSet are categories endowed with a weak factorization system---and indeed, an entire Quillen model structure---exhibiting the additional structure required for a homotopy-theoretic model is quite hard to do. However, the categories we are interested in share a number of common features, and abstracting these leads us to introduce the notion of a path object category. This is a relatively simple axiomatic framework, which is nonetheless sufficiently strong to allow the construction of homotopy-theoretic models. Now by exhibiting suitable path object structures on Top and SSet, we endow those categories with the structure of a homotopy-theoretic model and, in this way, obtain the desired topological and simplicial models of identity types.