2019/05/15 by Simon Henry, Henry, Simon · 1 citation
Computer Science · Mathematics · #18G30 #55U35 #55U40 #Advanced Topics in Algebra #Algebraic structures and combinatorial models #Category Theory (math.CT) #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic (math.LO) #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1905.06160
openalex publication_date 2019/05/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We give a fully constructive proof that there is a proper cartesian\n\ω-combinatorial model structure on the category of simplicial sets,\nwhose generating cofibrations and trivial cofibrations are the usual boundary\ninclusion and horn inclusion. The main difference with classical mathematics is\nthat constructively not all monomorphisms are cofibrations (only those\nsatisfying some decidability conditions) and not every object is cofibrant. The\nproof relies on three main ingredients: First, our construction of a weak model\ncategories on simplicial sets, then the interplay with the semi-simplicial\nversions of this weak model structure and finally, the use of Kan\nEx\∞-functor, and more precisely of S.Moss' direct proof that the\nnatural map X \→ Ex\∞ X is an anodyne morphism, which we\nshow is constructive when X is cofibrant.\n