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.
The PhD thesis of North @cite_4 uses a category-theoretic abstraction of the notion of Moore paths, called , as part of a complete analysis of when a weak factorization system gives a model (in terms of display map categories, rather than CwFs) of identity- , @math - and @math -types. A Moore relation system is a piece of category theory comparable to our use of ordered abelian groups in categorical logic in ; it would be interesting to see if it can be extended in the way we extended from groups to rings in in order to validate function extensionality.
@cite_4
2729164125
This article presents three characterizations of the weak factorization systems on finitely complete categories that interpret intensional dependent type theory with Sigma-, Pi-, and Id-types. The first characterization is that the weak factorization system (L,R) has the properties that L is stable under pullback along R and that all maps to a terminal object are in R. We call such weak factorization systems type-theoretic. The second is that the weak factorization system has an Id-presentation: roughly, it is generated by Id-types in the empty context. The third is that the weak factorization system (L, R) is generated by a Moore relation system, a generalization of the notion of Moore paths.