Models of Type Theory Based on Moore Paths

TL;DR

This paper develops a new class of models for intensional Martin-Löf type theory using Moore paths in toposes, featuring non-truncated structures without Kan filling conditions, advancing the understanding of identity types.

Contribution

It introduces a novel model based on Moore paths that avoids Kan filling conditions, expanding the landscape of non-truncated type-theoretic models.

Findings

Model contains non-trivial structure at all dimensions

Identity types are modeled by Moore paths

Avoids Kan filling conditions in semantics

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.