Non-Standard Models of Homotopy Type Theory

TL;DR

This paper introduces the filter quotient construction as a new method for creating models of homotopy type theory, capable of producing diverse models with unique properties, expanding the landscape of existing models.

Contribution

It proposes the filter quotient construction as a novel technique to generate new models of homotopy type theory that preserve key properties while diverging in set-theoretic aspects.

Findings

Filter quotient preserves model categorical properties for type constructors.

It does not preserve set-theoretic properties like cocompleteness.

Enables construction of diverse, previously unexplored models.

Abstract

Homotopy type theory is a modern foundation for mathematics that introduces the univalence axiom and is particularly suitable for the study of homotopical mathematics and its formalization via proof assistants. In order to better comprehend the mathematical implications of homotopy type theory, a variety of models have been constructed and studied. Here a model is understood as a model category with suitable properties implementing the various type theoretical constructors and axioms. A first example is the simplicial model due to Kapulkin--Lumsdaine--Voevodsky. By now, many other models have been constructed, due to work of Arndt, Kapulkin, Lumsdaine, Warren and particularly Shulman, culminating in a proof that every Grothendieck $\infty$-topos can be obtained as the underlying $\infty$-category of a model category that models homotopy type theory. In this paper we propose the filter quotient construction as a new method to construct further models of homotopy type theory. Concretely, we prove that with minor assumptions, the filter quotient construction preserves all model categorical properties individually that implement various type theoretical constructors and axioms. On the other hand, the filter quotient construction does not preserve many external properties that are of set theoretical nature, such as cocompleteness, local presentability or cofibrant generation. Combining these, the filter quotient construction preserves models of homotopy type theory and can result in models that have not been considered before and exhibit behaviors that diverge from any of the established models.