A co-reflection of cubical sets into simplicial sets with applications to model structures

Chris Kapulkin; Liang Ze Wong; Zachery Lindsey

arxiv: 1906.09203 · v1 · pith:KEQEBUJNnew · submitted 2019-06-21 · 🧮 math.CT · math.AT

A co-reflection of cubical sets into simplicial sets with applications to model structures

Chris Kapulkin , Zachery Lindsey , Liang Ze Wong This is my paper

Pith reviewed 2026-05-25 18:13 UTC · model grok-4.3

classification 🧮 math.CT math.AT

keywords cubical setssimplicial setsco-reflectionstraightening functormodel structuresQuillen model structureJoyal model structure

0 comments

The pith

Simplicial sets form a co-reflective subcategory of cubical sets with connections via the straightening functor.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proves that the category of simplicial sets sits as a co-reflective subcategory inside the category of cubical sets with connections. The co-reflection is realized by a version of the straightening functor that serves as the left adjoint to the inclusion. This co-reflector then supplies a transfer theorem that moves any cofibrantly generated model structure whose cofibrations are monomorphisms from simplicial sets to cubical sets. The construction produces explicit cubical versions of both the Quillen model structure and the Joyal model structure.

Core claim

The category of simplicial sets is a co-reflective subcategory of the category of cubical sets with connections, with the inclusion given by a version of the straightening functor. Using the co-reflector, any cofibrantly generated model structure in which cofibrations are monomorphisms transfers to cubical sets, yielding cubical analogues of the Quillen and Joyal model structures.

What carries the argument

The straightening functor, left adjoint to the inclusion of simplicial sets into cubical sets with connections, that acts as the co-reflector and enables transfer of model structures.

If this is right

Cubical sets carry a transferred Quillen model structure.
Cubical sets carry a transferred Joyal model structure.
Any cofibrantly generated model structure on simplicial sets whose cofibrations are monomorphisms yields a corresponding model structure on cubical sets.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same transfer technique may apply to other combinatorial models of spaces once a suitable co-reflection is identified.
Comparisons between simplicial and cubical homotopy theories can now proceed by lifting structures along the co-reflector rather than constructing them separately.

Load-bearing premise

The version of the straightening functor is left adjoint to the inclusion and the model structures satisfy the conditions needed for the transfer theorem to apply.

What would settle it

An explicit computation showing that the straightening functor fails to be left adjoint to the inclusion, or that the transferred structure on cubical sets violates one of the model category axioms for the Quillen case, would falsify the claims.

read the original abstract

We show that the category of simplicial sets is a co-reflective subcategory of the category of cubical sets with connections, with the inclusion given by a version of the straightening functor. We show that using the co-reflector, one can transfer any cofibrantly generated model structure in which cofibrations are monomorphisms to cubical sets, thus obtaining cubical analogues of the Quillen and Joyal model structures.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a concrete co-reflection from cubical sets with connections to simplicial sets via straightening that transfers cofibrantly generated model structures with mono cofibrations.

read the letter

The main takeaway is that simplicial sets form a co-reflective subcategory of cubical sets with connections, with the co-reflector given by a straightening functor, and this adjunction lets you move any cofibrantly generated model structure whose cofibrations are monomorphisms over to the cubical side. That produces cubical versions of the Quillen and Joyal model structures. The new piece is the explicit identification of this particular co-reflection and the check that the transfer theorem applies here. The transfer step itself follows from standard results once the adjunction is in place, so the work sits in spelling out the functor and confirming the hypotheses. It does a clean job of giving a direct tool for moving between these two shape categories without having to rebuild the model structures from scratch each time. For readers who already use cubical sets in homotopy theory, this removes some friction. The soft spot is that everything rests on the straightening functor satisfying the left-adjoint condition with counit isomorphism and on it preserving the generating (acyclic) cofibrations or the small-object-argument requirements. The abstract states that these verifications are done, and the overall argument structure is the usual one with no visible internal contradictions, but the result stands or falls on those lemmas being correct and not missing some interaction with the connections. This paper is aimed at people working with model categories on simplicial or cubical sets. A reader who needs to transfer structures between the two categories gets practical value from it. It deserves a serious referee so the adjunction and the transfer checks can be examined in detail.

Referee Report

1 major / 0 minor

Summary. The paper claims that the category of simplicial sets is a co-reflective subcategory of the category of cubical sets with connections, with the inclusion realized by a version of the straightening functor. It further claims that the resulting co-reflector permits the transfer of any cofibrantly generated model structure whose cofibrations are monomorphisms, thereby producing cubical analogues of the Quillen and Joyal model structures.

Significance. If the stated adjunction and transfer results hold with the required verifications, the work would supply a systematic mechanism for moving model structures between simplicial and cubical settings, which is of interest for comparing homotopy theories and for constructing new model categories on cubical sets.

major comments (1)

[Abstract] Abstract: the text asserts that proofs exist for the co-reflection (via the straightening functor) and for the transfer of model structures, but supplies no lemmas, equations, or verification steps; the central claims therefore cannot be checked from the given material.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their report. We address the single major comment below.

read point-by-point responses

Referee: [Abstract] Abstract: the text asserts that proofs exist for the co-reflection (via the straightening functor) and for the transfer of model structures, but supplies no lemmas, equations, or verification steps; the central claims therefore cannot be checked from the given material.

Authors: The abstract is a concise summary of the main theorems and is not intended to contain the detailed proofs. The full manuscript develops the straightening functor, proves the co-reflection, and verifies the transfer of cofibrantly generated model structures with monomorphisms as cofibrations (including the cubical Quillen and Joyal structures). These arguments appear in the body with the requisite lemmas and verifications. revision: no

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper proves that simplicial sets form a co-reflective subcategory of cubical sets with connections via a straightening functor, then transfers cofibrantly generated model structures with monic cofibrations. This relies on direct verification of adjunction properties (counit isomorphism) and application of an external transfer theorem. No self-definitional reductions, fitted inputs renamed as predictions, load-bearing self-citations, or imported uniqueness theorems appear. The argument is a standard categorical construction verifiable independently of the paper's own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review; no explicit free parameters, axioms, or invented entities are stated.

pith-pipeline@v0.9.0 · 5591 in / 1061 out tokens · 20835 ms · 2026-05-25T18:13:39.127020+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

13 extracted references · 13 canonical work pages

[1]

write newline

" write newline "" before.all 'output.state := FUNCTION output.nonempty.mrnumber duplicate missing pop "" 'skip if duplicate empty 'pop " " swap * " " * write if FUNCTION fin.entry.original add.period write newline INTEGERS nameptr namesleft numnames FUNCTION format.language language empty "" " (" language * ")" * if FUNCTION format.names 's := #1 'namept...

work page
[2]

Leibniz Int

Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\" o rtberg, Cubical type theory: a constructive interpretation of the univalence axiom, 21st I nternational C onference on T ypes for P roofs and P rograms, LIPIcs. Leibniz Int. Proc. Inform., vol. 69, Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2018, pp. Art. No. 5, 34

work page 2018
[3]

308, xxiv+390

Denis-Charles Cisinski, Les pr\'efaisceaux comme mod\`eles des types d'homotopie, Ast\'erisque (2006), no. 308, xxiv+390

work page 2006
[4]

, Univalent universes for elegant models of homotopy types, 2014, http://arxiv.org/abs/406.0058 arXiv:406.0058

work page 2014
[5]

Richard Garner, Magdalena K e dziorek, and Emily Riehl, Lifting accessible model structures, preprint, 2018, http://arxiv.org/abs/1802.09889 arXiv:1802.09889

work page arXiv 2018
[6]

Marco Grandis and Luca Mauri, Cubical sets and their site, Theory Appl. Categ. 11 (2003), No. 8, 185--211

work page 2003
[7]

Kathryn Hess, Magdalena K e dziorek, Emily Riehl, and Brooke Shipley, A necessary and sufficient condition for induced model structures, J. Topol. 10 (2017), no. 2, 324--369, http://dx.doi.org/10.1112/topo.12011 doi:10.1112/topo.12011

work page doi:10.1112/topo.12011 2017
[8]

Jardine, Categorical homotopy theory, Homology, Homotopy Appl

John F. Jardine, Categorical homotopy theory, Homology, Homotopy Appl. 8 (2006), no. 1, 71--144, http://projecteuclid.org/euclid.hha/1140012467

work page arXiv 2006
[9]

Kan, Abstract homotopy

Daniel M. Kan, Abstract homotopy. I , Proc. Nat. Acad. Sci. U.S.A. 41 (1955), 1092--1096

work page 1955
[10]

Sanjeevi Krishnan, Cubical approximation for directed topology I , Appl. Categ. Structures 23 (2015), no. 2, 177--214, http://dx.doi.org/10.1007/s10485-013-9330-y doi:10.1007/s10485-013-9330-y , https://doi.org/10.1007/s10485-013-9330-y

work page doi:10.1007/s10485-013-9330-y 2015
[11]

Krzysztof Kapulkin and Vladimir Voevodsky, Cubical approach to straightening, submitted, available from authors' websites, 2018

work page 2018
[12]

11 (2009), no

Georges Maltsiniotis, La cat\'egorie cubique avec connexions est une cat\'egorie test stricte, Homology, Homotopy Appl. 11 (2009), no. 2, 309--326, http://projecteuclid.org/euclid.hha/1296138523

work page arXiv 2009
[13]

5, Springer-Verlag, New York, 1998

Saunders Mac Lane, Categories for the working mathematician, 2 ed., Graduate Texts in Mathematics, vol. 5, Springer-Verlag, New York, 1998

work page 1998

[1] [1]

write newline

" write newline "" before.all 'output.state := FUNCTION output.nonempty.mrnumber duplicate missing pop "" 'skip if duplicate empty 'pop " " swap * " " * write if FUNCTION fin.entry.original add.period write newline INTEGERS nameptr namesleft numnames FUNCTION format.language language empty "" " (" language * ")" * if FUNCTION format.names 's := #1 'namept...

work page

[2] [2]

Leibniz Int

Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\" o rtberg, Cubical type theory: a constructive interpretation of the univalence axiom, 21st I nternational C onference on T ypes for P roofs and P rograms, LIPIcs. Leibniz Int. Proc. Inform., vol. 69, Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2018, pp. Art. No. 5, 34

work page 2018

[3] [3]

308, xxiv+390

Denis-Charles Cisinski, Les pr\'efaisceaux comme mod\`eles des types d'homotopie, Ast\'erisque (2006), no. 308, xxiv+390

work page 2006

[4] [4]

, Univalent universes for elegant models of homotopy types, 2014, http://arxiv.org/abs/406.0058 arXiv:406.0058

work page 2014

[5] [5]

Richard Garner, Magdalena K e dziorek, and Emily Riehl, Lifting accessible model structures, preprint, 2018, http://arxiv.org/abs/1802.09889 arXiv:1802.09889

work page arXiv 2018

[6] [6]

Marco Grandis and Luca Mauri, Cubical sets and their site, Theory Appl. Categ. 11 (2003), No. 8, 185--211

work page 2003

[7] [7]

Kathryn Hess, Magdalena K e dziorek, Emily Riehl, and Brooke Shipley, A necessary and sufficient condition for induced model structures, J. Topol. 10 (2017), no. 2, 324--369, http://dx.doi.org/10.1112/topo.12011 doi:10.1112/topo.12011

work page doi:10.1112/topo.12011 2017

[8] [8]

Jardine, Categorical homotopy theory, Homology, Homotopy Appl

John F. Jardine, Categorical homotopy theory, Homology, Homotopy Appl. 8 (2006), no. 1, 71--144, http://projecteuclid.org/euclid.hha/1140012467

work page arXiv 2006

[9] [9]

Kan, Abstract homotopy

Daniel M. Kan, Abstract homotopy. I , Proc. Nat. Acad. Sci. U.S.A. 41 (1955), 1092--1096

work page 1955

[10] [10]

Sanjeevi Krishnan, Cubical approximation for directed topology I , Appl. Categ. Structures 23 (2015), no. 2, 177--214, http://dx.doi.org/10.1007/s10485-013-9330-y doi:10.1007/s10485-013-9330-y , https://doi.org/10.1007/s10485-013-9330-y

work page doi:10.1007/s10485-013-9330-y 2015

[11] [11]

Krzysztof Kapulkin and Vladimir Voevodsky, Cubical approach to straightening, submitted, available from authors' websites, 2018

work page 2018

[12] [12]

11 (2009), no

Georges Maltsiniotis, La cat\'egorie cubique avec connexions est une cat\'egorie test stricte, Homology, Homotopy Appl. 11 (2009), no. 2, 309--326, http://projecteuclid.org/euclid.hha/1296138523

work page arXiv 2009

[13] [13]

5, Springer-Verlag, New York, 1998

Saunders Mac Lane, Categories for the working mathematician, 2 ed., Graduate Texts in Mathematics, vol. 5, Springer-Verlag, New York, 1998

work page 1998