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 -