The derivator of setoids
From MaRDI portal
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.
Recommendations
- The fullness axiom and exact completion of homotopy categories
- Exact completion and constructive theories of sets
- Exact completion of path categories and algebraic set theory. I: Exact completion of path categories
- Constructing categories and setoids of setoids in type theory
- Universal properties and derived Kan extensions
Cited in
(6)
This page was built for publication: The derivator of setoids
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5870839)
