Models of Type Theory Based on Moore Paths

Richard Orton & Andrew Pitts
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...
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.