TY - GEN
T1 - Formalizing the Algebraic Small Object Argument in UniMath
AU - Hilhorst, Dennis
AU - North, Paige Randall
N1 - Publisher Copyright:
© 2024 Dennis Hilhorst and Paige Randall North.
PY - 2024/9/2
Y1 - 2024/9/2
N2 - 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.
AB - 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.
KW - algebraic small object argument
KW - coq
KW - formalization of mathematics
KW - model category theory
KW - unimath
KW - univalent foundations
UR - http://www.scopus.com/inward/record.url?scp=85204094997&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.ITP.2024.20
DO - 10.4230/LIPIcs.ITP.2024.20
M3 - Conference contribution
AN - SCOPUS:85204094997
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 15th International Conference on Interactive Theorem Proving, ITP 2024
A2 - Bertot, Yves
A2 - Kutsia, Temur
A2 - Norrish, Michael
PB - Dagstuhl Publishing
T2 - 15th International Conference on Interactive Theorem Proving, ITP 2024
Y2 - 9 September 2024 through 14 September 2024
ER -