The Fullness Axiom and exact completion of homotopy categories

TL;DR

This paper employs a category-theoretic approach to derive local cartesian closure of exact completions in homotopy categories, connecting constructive set theory principles with homotopy theory.

Contribution

It introduces a category-theoretic formulation of Aczel's Fullness Axiom and applies it to establish local cartesian closure in homotopy categories, including those of topological spaces.

Findings

Local cartesian closure of the exact completion of homotopy categories.

Validation of the Fullness Axiom in models satisfying mild conditions.

Application to the category of setoids under a type-theoretic perspective.

Abstract

We use a category-theoretic formulation of Aczel's Fullness Axiom from Constructive Set Theory to derive the local cartesian closure of an exact completion. As an application, we prove that such a formulation is valid in the homotopy category of any model category satisfying mild requirements, thus obtaining in particular the local cartesian closure of the exact completion of topological spaces and homotopy classes of maps. Under a type-theoretic reading, these results provide a general motivation for the local cartesian closure of the category of setoids. However, results and proofs are formulated solely in the language of categories, and no knowledge of type theory or constructive set theory is required on the reader's part.