A homotopy-theoretic model of function extensionality in the effective topos

TL;DR

This paper constructs a homotopy-theoretic model of function extensionality within the effective topos, using a novel approach that does not require cocompleteness, and analyzes its implications for type theory and categorical structures.

Contribution

It introduces a new method for building a Quillen model structure on an elementary topos using an interval object, applicable to the effective topos, and explores its properties and connections to existing models.

Findings

Uniform inhabited objects are contractible.

Discrete objects are fibrant.

The homotopy category of fibrant assemblies is equivalent to modest sets.

Abstract

We present a way of constructing a Quillen model structure on a full subcategory of an elementary topos, starting with an interval object with connections and a certain dominance. The advantage of this method is that it does not require the underlying topos to be cocomplete. The resulting model category structure gives rise to a model of homotopy type theory with identity types, $\Sigma$- and $\Pi$-types, and functional extensionality. We apply the method to the effective topos with the interval object $\nabla 2$. In the resulting model structure we identify uniform inhabited objects as contractible objects, and show that discrete objects are fibrant. Moreover, we show that the unit of the discrete reflection is a homotopy equivalence and the homotopy category of fibrant assemblies is equivalent to the category of modest sets. We compare our work with the path object category construction on the effective topos by Jaap van Oosten.