Formalizing the algebraic small object argument in UniMath

DOI10.4230/LIPICS.ITP.2024.20MaRDI QIDQ6860011zbMATH OpenFDO

Authors Dennis Hilhorst, Paige Randall North

Publication date 10 February 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2024.20

zbMATH Keywords

algebraic small object argumentCoqformalization of mathematicsmodel category theoryUniMathunivalent foundations

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• \(\mathbb{A}^1\)-homotopy theory of schemes
• A model for the homotopy theory of homotopy theory
• A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on
• Displayed categories
• Homotopy theoretic models of identity types
• MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
• Natural weak factorization systems.
• Set-theoretic and type-theoretic ordinals coincide
• Strong stacks and classifying spaces
• Towards a constructive simplicial model of Univalent Foundations
• Understanding the small object argument
• Unifying Cubical Models of Univalent Type Theory
• Univalent categories and the Rezk completion
• Univalent monoidal categories

This page was built for publication: Formalizing the algebraic small object argument in UniMath

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6860011)