Document Open Access Logo

Formalizing the Algebraic Small Object Argument in UniMath

Authors Dennis Hilhorst , Paige Randall North

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.20.pdf
  • Filesize: 0.9 MB
  • 18 pages

Document Identifiers

Author Details

Dennis Hilhorst
  • Department of Mathematics, Utrecht University, The Netherlands
Paige Randall North
  • Department of Information and Computing Sciences, Department of Mathematics, Utrecht University, The Netherlands

Funding

  • North, Paige Randall: This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0334.

Cite As Get BibTex

Dennis Hilhorst and Paige Randall North. Formalizing the Algebraic Small Object Argument in UniMath. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.ITP.2024.20

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • formalization of mathematics
  • univalent foundations
  • model category theory
  • algebraic small object argument
  • coq
  • unimath

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Benedikt Ahrens, Kapulkin Krzysztof, and Michael Shulman. Univalent categories and the rezk completion. Mathematical Structures in Computer Science, 25(5):1010-1039, 2015. URL: https://doi.org/10.1017/S0960129514000486.
  2. Benedikt Ahrens and Peter LeFanu Lumsdaine. Displayed categories. Logical Methods in Computer Science, Volume 15, Issue 1, May 2017. URL: https://doi.org/10.23638/LMCS-15(1:20)2019.
  3. Benedikt Ahrens, Ralph Matthes, and Kobe Wullaert. Formalizing monoidal categories and actions for syntax with binders, 2023. URL: https://arxiv.org/abs/2307.16270.
  4. Benedikt Ahrens, Paige Randall North, Michael Shulman, and Dimitris Tsementzis. The Univalence Principle, 2022. URL: https://arxiv.org/abs/2102.06275.
  5. Steve Awodey. A cubical model of homotopy type theory, 2016. URL: https://arxiv.org/abs/1607.06413.
  6. Steve Awodey. Cartesian cubical model categories, 2023. URL: https://arxiv.org/abs/2305.00893.
  7. Steve Awodey and Michael A. Warren. Homotopy theoretic models of identity types. Math. Proc. Cambridge Philos. Soc., 146(1):45-55, 2009. URL: https://doi.org/10.1017/S0305004108001783.
  8. Evan Cavallo, Anders Mörtberg, and Andrew W Swan. Unifying Cubical Models of Univalent Type Theory. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020), volume 152 of Leibniz International Proceedings in Informatics (LIPIcs), pages 14:1-14:17, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.14.
  9. Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu. Set-theoretic and type-theoretic ordinals coincide. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, June 2023. URL: https://doi.org/10.1109/lics56636.2023.10175762.
  10. Nicola Gambino and Simon Henry. Towards a constructive simplicial model of Univalent Foundations. Journal of the London Mathematical Society, 105(2):1073-1109, 2022. URL: https://doi.org/10.1112/jlms.12532.
  11. Nicola Gambino and Marco Federico Larrea. Models of Martin-Löf type theory from algebraic weak factorisation systems. The Journal of Symbolic Logic, 88(1):242-289, June 2021. URL: https://doi.org/10.1017/jsl.2021.39.
  12. Richard Garner. Cofibrantly generated natural weak factorisation systems, 2007. URL: https://arxiv.org/abs/math/0702290.
  13. Richard Garner. Understanding the small object argument. Applied Categorical Structures, 17(3):247-285, April 2008. URL: https://doi.org/10.1007/s10485-008-9137-4.
  14. Marco Grandis and Walter Tholen. Natural weak factorization systems. Archivum Mathematicum, 42, January 2006. Google Scholar
  15. Dennis Hilhorst. A Formalization of the Algebraic Small Object Argument in UniMath, November 2023. Available at URL: https://studenttheses.uu.nl/handle/20.500.12932/45658.
  16. Mark Hovey. Model Categories. Mathematical surveys and monographs. American Mathematical Society, 2007. Google Scholar
  17. André Joyal. Notes on quasi-categories. Preprint, 2008. Google Scholar
  18. André Joyal and Myles Tierney. Strong stacks and classifying spaces. In Aurelio Carboni, Maria Cristina Pedicchio, and Guiseppe Rosolini, editors, Category Theory, pages 213-236, Berlin, Heidelberg, 1991. Springer Berlin Heidelberg. Google Scholar
  19. Chris Kapulkin and Peter LeFanu Lumsdaine. The Simplicial Model of Univalent Foundations (after Voevodsky), 2018. URL: https://arxiv.org/abs/1211.2851.
  20. G. M. Kelly. A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on. Bulletin of the Australian Mathematical Society, 22(1):1-83, 1980. URL: https://doi.org/10.1017/S0004972700006353.
  21. Jacob Lurie. Derived Algebraic Geometry III: Commutative Algebra, 2009. URL: https://arxiv.org/abs/math/0703204.
  22. J. P. May and K. Ponto. More Concise Algebraic Topology: Localization, Completion, and Model Categories. University of Chicago Press, Chicago, 2011. URL: https://cds.cern.ch/record/1416976.
  23. Fabien Morel and Vladimir Voevodsky. A¹-homotopy theory of schemes. Publications Mathématiques de l'IHÉS, 90:45-143, 1999. Google Scholar
  24. nLab authors. weak factorization system. Available at https://ncatlab.org/nlab/show/weak+factorization+system, March 2024. URL: https://ncatlab.org/nlab/revision/weak+factorization+system/46.
  25. Daniel G. Quillen. Homotopical Algebra. Lecture notes in mathematics. Springer-Verlag, 1967. Google Scholar
  26. Charles Rezk. A model for the homotopy theory of homotopy theory. Transactions of the American Mathematical Society, 353(3):973-1007, 2001. Google Scholar
  27. Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. Unimath - a computer-checked library of univalent mathematics. Available at http://unimath.org. URL: https://doi.org/10.5281/zenodo.7848572.
  28. Kobe Wullaert, Ralph Matthes, and Benedikt Ahrens. Univalent Monoidal Categories. In Delia Kesner and Pierre-Marie Pédrot, editors, 28th International Conference on Types for Proofs and Programs (TYPES 2022), volume 269 of Leibniz International Proceedings in Informatics (LIPIcs), pages 15:1-15:21, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2022.15.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact