The derivator of setoids

TL;DR

This paper constructs a derivator structure for the category of setoids without relying on the axiom of choice, revealing implications for constructive homotopy theory and the nature of setoids.

Contribution

It demonstrates that the category of setoids can be enhanced to a derivator, providing a new universal cocompletion perspective in constructive mathematics.

Findings

The derivator of setoids can be constructed without the axiom of choice.

This derivator is the free cocompletion of a point among 1-truncated derivators.

Implications suggest setoids are essential in constructive homotopy theory.

Abstract

Without the axiom of choice, the free exact completion of the category of sets (i.e. the category of setoids) may not be complete or cocomplete. We will show that nevertheless, it can be enhanced to a derivator: the formal structure of categories of diagrams related by Kan extension functors. Moreover, this derivator is the free cocompletion of a point in a class of "1-truncated derivators" (which behave like a 1-category rather than a higher category). In classical mathematics, the free cocompletion of a point relative to all derivators is the homotopy theory of spaces. Thus, if there is a homotopy theory that can be shown to have this universal property constructively, its 1-truncation must contain not only sets, but also setoids. This suggests that either setoids are an unavoidable aspect of constructive homotopy theory, or more radical modifications to the notion of homotopy theory are needed.