2026-07-21T14:10:49Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24618 2025-12-12T15:10:01Z ddc:004 open_access

Formalizing Colimits in 𝒞at Carneiro, Mario Riehl, Emily category theory infinity-category theory nerve simplicial set colimit Certain results involving "higher structures" are not currently accessible to computer formalization because the prerequisite ∞-category theory has not been formalized. To support future work on formalizing ∞-category theory in Lean’s mathematics library, we formalize some fundamental constructions involving the 1-category of categories. Specifically, we construct the left adjoint to the nerve embedding of categories into simplicial sets, defining the homotopy category functor. We prove further that this adjunction is reflective, which allows us to conclude that 𝒞at has colimits. To our knowledge this is the first formalized proof that the nerve functor is a fully faithful right adjoint and that the category of categories is cocomplete. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Mario Carneiro and Emily Riehl 2025 Is Part Of LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2025.20 urn:nbn:de:0030-drops-246186 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.20 eng https://creativecommons.org/licenses/by/4.0/legalcode