Formalizing the Algebraic Small Object Argument in UniMath

Dennis Hilhorst*, Paige Randall North*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

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.

Original languageEnglish
Title of host publication15th International Conference on Interactive Theorem Proving, ITP 2024
EditorsYves Bertot, Temur Kutsia, Michael Norrish
PublisherDagstuhl Publishing
Number of pages18
ISBN (Electronic)9783959773379
DOIs
Publication statusPublished - 2 Sept 2024
Event15th International Conference on Interactive Theorem Proving, ITP 2024 - Tbilisi, Georgia
Duration: 9 Sept 202414 Sept 2024

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume309
ISSN (Print)1868-8969

Conference

Conference15th International Conference on Interactive Theorem Proving, ITP 2024
Country/TerritoryGeorgia
CityTbilisi
Period9/09/2414/09/24

Keywords

  • algebraic small object argument
  • coq
  • formalization of mathematics
  • model category theory
  • unimath
  • univalent foundations

Fingerprint

Dive into the research topics of 'Formalizing the Algebraic Small Object Argument in UniMath'. Together they form a unique fingerprint.

Cite this