The derivator of setoids

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.

arXiv comment42 pages. v2: Clarified discussion of anafunctors and anaderivators

References in corpus (11)

• Univalent categories and the Rezk completion
• The Simplicial Model of Univalent Foundations (after Voevodsky)
• Higher gauge theory I: 2-Bundles
• Two-Level Type Theory and Applications
• Internal categories, anafunctors and localisations
• Towards a constructive simplicial model of Univalent Foundations
• Weak model categories in classical and constructive mathematics
• The constructive Kan-Quillen model structure: two new proofs
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• The elementary construction of formal anafunctors
• A constructive account of the Kan-Quillen model structure and of Kan's Ex${}^{\infty }$ functor