eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-09-02
20:1
20:18
10.4230/LIPIcs.ITP.2024.20
article
Formalizing the Algebraic Small Object Argument in UniMath
Hilhorst, Dennis
1
https://orcid.org/0009-0000-9823-9885
North, Paige Randall
2
https://orcid.org/0000-0001-7876-0956
Department of Mathematics, Utrecht University, The Netherlands
Department of Information and Computing Sciences, Department of Mathematics, Utrecht University, The Netherlands
Quillen model category theory forms the cornerstone of modern homotopy theory, and thus the semantics of (and justification for the name of) homotopy type theory / univalent foundations (HoTT/UF). One of the main tools of Quillen model category theory is the small object argument. Indeed, the particular model categories that can interpret HoTT/UF are usually constructed using the small object argument.
In this article, we formalize the algebraic small object argument, a modern categorical version of the small object argument originally due to Garner, in the Coq UniMath library. This constitutes a first step in building up the tools required to formalize - in a system based on HoTT/UF - the semantics of HoTT/UF in particular model categories: for instance, Voevodsky’s original interpretation into simplicial sets.
More specifically, in this work, we rephrase and formalize Garner’s original formulation of the algebraic small object argument. We fill in details of Garner’s construction and redefine parts of the construction to be more direct and fit for formalization. We rephrase the theory in more modern language, using constructions like displayed categories and a modern, less strict notion of monoidal categories. We point out the interaction between the theory and the foundations, and motivate the use of the algebraic small object argument in lieu of Quillen’s original small object argument from a constructivist standpoint.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol309-itp2024/LIPIcs.ITP.2024.20/LIPIcs.ITP.2024.20.pdf
formalization of mathematics
univalent foundations
model category theory
algebraic small object argument
coq
unimath