{"id":"210b14fe-6603-42e4-b4d7-e8ccfd39a2fd","arxiv_id":"1908.06201","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Homotopy colimits in the vertical simplicially enriched category of a higher equipment coincide with double colimits of companion diagrams, unifying double category theory with homotopy theory.","lead":"Simplicial categories, collections of categories varying in extra dimensions, are treated as two-way categorical structures, and the paper shows that homotopy colimits, the standard way to glue spaces up to homotopy, arise as double colimits in these structures. It offers a unifying framework that could connect double category theory with homotopy theory.","discovery_kind":"unification","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Equipment property for sSet^♯ is asserted via an unverified pushout; for n≥3 the pushout can produce faces larger than the prescribed Y_i, undermining Theorem 4.","rationale":"The reader's weakest_assumption isolates Definition 4, and my reading agrees: the entire higher-equipment construction runs on the universal extension property of Definition 4. If that property fails for sSet^♯, the paper's motivating example and Theorem 4's application to homotopy colimits of spaces collapse. My reading of §3.2 found a specific unverified point rather than a stylistic worry: the pushout diagram Y=X∐_{∂X}Y• presupposes that the compatible family (Y_i,f_i) can be glued into an object over ∂Δ^n and that gluing preserves the prescribed face restrictions. For n≥3, the compatibility equations do not provide the needed identifications between Y_i and Y_j over shared subfaces, and a colimit construction can enlarge the faces. The proposed check with an extra 1-simplex in Y_1 is designed to settle this. I therefore do not see the present text as establishing the central claim; it needs either a completed verification of Definition 4 for sSet^♯ or a corrected statement. A second gap—the proof of Theorem 4 only handles J=Δ^n and does not check compatibility over Gro(J)—would also need to be addressed, but it is secondary to the equipment property. This matches the reader's CONDITIONAL verdict; I do not recommend a harsher verdict because the gap is concrete but potentially repairable, and the framework may be sound with additional hypotheses. The paper contains some independent value: the Grothendieck construction as a double colimit in Prof (Theorem 1) is argued carefully, and the vertical sSet-category construction is a reasonable definition. But these do not by themselves support Theorem 4.","tokens_in":29905,"tokens_out":24605,"duration_ms":251189,"concrete_test":"Concrete check for Definition 4 with n=3 in sSet^♯. Set X=Δ^3→Δ^3. Let Y_0=d_0X, Y_2=d_2X, Y_3=d_3X with f_i the face inclusions. Let Y_1 = d_1X ∐ Δ^1, where the extra Δ^1 summand maps to the edge {2,3} = d_0∩d_1, and let f_1:d_1X→Y_1 be inclusion into the first summand. Check that the compatibility equations d_i f_j = d_{j−1} f_i hold for all i<j. Form Y• by gluing the Y_i along the face lattice of ∂Δ^3, then form Y = X ∐_{∂X} Y•. Compute d_0Y = Y ×_{Δ^3} Δ^2. If d_0Y is not isomorphic to Y_0—for instance if the detached Δ^1 summand of Y_1 persists in d_0Y—then Definition 4(i) fails for the paper's flagship example. If the computation instead yields d_0Y ≅ Y_0, then a proof of this face-preservation is still missing and should be supplied before Theorem 4 is relied upon.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central theorem (Theorem 4) depends on Definition 4: companions, the companion recursion in §3.3, and the tower representation in Proposition 5 all require the universal extension property. The verification of Definition 4 for the flagship example sSet^♯ is a one-line diagram in §3.2, essentially asserting that Y = X ∐_{∂X} Y• is the desired fill. Two unproved points are load-bearing. First, the compatible family (Y_i, f_i) must be assembled into a single object Y• over ∂Δ^n with d_iY• = Y_i; the compatibility condition d_i f_j = d_{j−1} f_i compares the restrictions of the source maps after applying face maps to the codomains, but it does not by itself give the required identifications between Y_i and Y_j over shared subfaces. Second, even when Y• is formed by the evident colimit over the face lattice, the face d_iY can be strictly larger than Y_i. Concretely, for n=3, if Y_1 contains an extra 1-simplex lying over the edge d_0∩d_1 that is not in the image of the shared edge under f_1, then the pushout Y has d_0Y = Y_0 ⊔ (that extra 1-simplex), not Y_0. Thus Definition 4(i) can fail for sSet^♯, which would deprive the paper of its main example and break the double-colimit side of Theorem 4. The text leaves the simplicial identities and face-preservation to intuition (§3.1), but these are precisely the steps on which the theorem rests.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a theory of higher equipments: simplicial categories E (simplicial objects in Cat) equipped with a universal extension property for maps from the boundary of an n-simplex, together with examples Cat^♯, sSet^♯, Top^♯ and coSpan(C)^♯. It defines companions of vertical simplices, double colimits of horizontal diagrams, and a vertical simplicially enriched category E_v. The main result, Theorem 4, asserts that for a higher equipment E, an indexing category J, and a functor F:J→E_0, the double colimit of the companion diagram F* is isomorphic to the homotopy colimit of F in E_v. The paper also states an adjunction between simplicial categories and sSet-categories and proposes the principle that simplicial categories are to simplicially enriched categories what double categories are to 2-categories.","tokens_in":30342,"tokens_out":9124,"duration_ms":91791,"significance":"The central analogy is attractive and, if fully established, would give a genuinely new double-categorical description of homotopy colimits. The paper is written in an expository spirit, with explicit definitions, illustrations, and helpful pedagogical passages. It also honestly flags some of its own limitations, such as the lack of a constructed simplicial category Set^♯. However, the main theorem is only sketched, and the equipment property for the flagship example sSet^♯ is asserted rather than proved. Since companions, the tower representation, and Theorem 4 all rest on the equipment property, the current manuscript does not yet substantiate its principal claims.","major_comments":[{"comment":"The verification of the equipment property for sSet^♯ is a single sentence: after displaying the pushout diagram, the text says 'Similarly Cat^♯, Top^♯ and coSpan(C)^♯ satisfy the equipment property.' This is load-bearing. For n≥3 the proposed pushout Y = X ∐_{∂X} Y• generally does not satisfy Definition 4(i). For example, when n=3, if Y_1 contains a 1-simplex over the common edge d_0∩d_1 that is not in the image of the corresponding edge of X under f_1, then d_0Y contains that extra simplex, so d_0Y ≠ Y_0. Thus the universal extension is not an object of sSet^♯_n with the prescribed faces. Because Definition 4 underlies the companion construction, Proposition 5, and Theorem 4, this gap is fundamental.","section":"§3.2, Definition 4"},{"comment":"The paper explicitly says that Cat^♯ and sSet^♯ are only weak simplicial categories: 'Verifying the simplcial identities (up to isomorphism) and coherence laws is an easy but tedious exercice' and d_1s_0≅1. However, Definition 4, the boundary notation ∂x, Proposition 3, the companion recursion in §3.3, and the construction of E_v all treat E as a strict simplicial category. There is no definition of a weak simplicial category and no explanation of how the universal extension property and the equations d_i y = y_i are to be interpreted when face functors compose only up to isomorphism. This ambiguity affects the well-definedness of σ* and of the vertical enrichment E_v.","section":"§3.1, §3.2, §3.3"},{"comment":"The proof of Theorem 4 is a one-paragraph sketch. It invokes Theorem 2, Proposition 5, and Proposition 6, but it does not verify that the composite F* is an oplax transformation satisfying the coherence conditions required by Definition 5, nor does it prove that the claimed isomorphism is natural. The statement that a morphism σ*→s^n y corresponds precisely to morphisms from the staircase diagram is asserted without checking the universal properties at each step. A complete proof must exhibit the double-colimit universal property explicitly and compare it with the mapping-cylinder description of homotopy colimits.","section":"§3.6, proof of Theorem 4"},{"comment":"Theorem 3 states that if E has double colimits then E_v is cotensored, but the proof actually defines K⊙x = dcolim K_x and derives the tensor isomorphism sSet(K, E_v(x,y)) ≅ E_v0(K⊙x,y). This is the tensor property, not the cotensor property; the dual statement, using double limits, gives cotensors. The misstatement matters because the homotopy colimit formula in §3.5 uses tensors, and the paper's use of tensors should be grounded in a correctly stated theorem.","section":"§3.5, §3.6, Theorem 3"},{"comment":"The companion construction is asserted to define an oplax transformation (·)*: E_0→E, but no proof is given that the comparison maps α_i satisfy the required naturality and coherence diagrams. The recursion indicates that the faces of s_i φ_σ factor through the faces of φ_{s_i σ}, but the coherence laws for the α_i are not demonstrated. This coherence is essential because Theorem 4 composes F:J→E_0 with (·)* to produce the horizontal diagram F* whose double colimit is computed.","section":"§3.3, companion construction"}],"minor_comments":[{"comment":"In the discussion of collages, the text says 'with p^{-1}(0)=C and p^{-1}(0)=D'; the second occurrence should be p^{-1}(1)=D.","section":"§1"},{"comment":"The notation X(n) for the set of n-simplices of a simplicial set X conflicts with the earlier convention X_n and should be standardized.","section":"§3.1"},{"comment":"In the definition of an n-collage, the displayed formula ob(C)=∐_{i=1}^n ob(C_i) should be indexed from i=0 to n, since the tuple is (C_0,...,C_n,C).","section":"§3.1, Definition 3"},{"comment":"In the duality discussion, the sentence 'and the homotopy colimit on the left side is interpreted' should refer to the homotopy limit, since the equation displayed is dlim *F ≅ holim F.","section":"§3.7"},{"comment":"In the proof of Proposition 2, the statement that verifying the universal property is 'an easy exercise' leaves the uniqueness clause unaddressed; the proof would be more complete if the universal property were written out.","section":"§2.5.2"}],"recommendation":"reject","confidential_remarks":"The paper has a promising expository frame, but the central mathematical claim is not established. Most importantly, the equipment property for sSet^♯ appears to fail by the pushout construction for n≥3, which would remove the paper's main example. Fixing this would require either changing the definition of the examples or reformulating the equipment property, which is beyond a local revision. The current manuscript reads as a preliminary sketch rather than a completed proof, and I do not see how it can be accepted without substantial reworking."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"If you look at this paper, the thing to know is that it has a real idea and then leaves it largely unproven. The central construction—a simplicial category sSet^♯ with n-simplices the slice category sSet/Δ^n—and the slogan that simplicial categories are to sSet-categories what double categories are to 2-categories are worth taking seriously. The expository build-up from collages to equipments is clear, and the Grothendieck construction as a double colimit (Theorem 1) is plausible and adequately sketched.\n\nThe problem is the equipment property. Definition 4 requires that for a coherent family of maps from the faces of x to objects y_i, the universal extension y satisfies d_i y = y_i. For sSet^♯ this is asserted via a one-line pushout, but the pushout does not obviously produce that equality. I checked the stress-test concern and it lands: when n = 3, if Y_1 has an extra simplex over an edge shared with Y_0, that simplex survives in the face d_0 of the pushout, so d_0 Y contains Y_0 plus extra stuff. The compatibility condition d_i f_j = d_{j-1} f_i only identifies the images of the source under the two maps; it does not force Y_i and Y_j to have the same extra data on shared subfaces. So the flagship example may fail the equipment property as stated. Since companions, the tower representation, and Theorem 4 all depend on that property, this is load-bearing, not a cosmetic gap.\n\nThere is also a strictness issue. The paper admits the simplicial identities for Cat^♯ and sSet^♯ hold only up to isomorphism, yet everything is written as if E is a strict simplicial category. No definition of a weak simplicial category or coherence theorem is supplied. And the proof of Theorem 4 is a paragraph: for J = Δ^n it says the tower representation plus Proposition 6 imply the correspondence, without spelling out the verification. That is a sketch, not a proof.\n\nWhat is genuinely good here: the intuition that companions are mapping cylinders, that double colimits of companions compute homotopy colimits, and that the vertical enrichment of a simplicial category is a sSet-category. These are worth developing. But as it stands, the paper is a program with the main theorem unsupported. I would not cite it for the central result yet.\n\nWho is this for? Category theorists working on equipments or double categorical frameworks for homotopy theory, and perhaps graduate students who want a readable introduction to the motivations. A serious referee should see it—conditional acceptance with major revision is the right call, not desk rejection. The author needs to either fix the equipment property (maybe by requiring the Y_i to agree on all overlaps as objects, or by weakening the equality to an isomorphism and proving coherence) or find a different class of examples. The idea deserves another pass.","headline":"A genuinely promising unifying idea whose central theorem currently rests on an unproved (and likely false as stated) equipment property for sSet^♯.","tokens_in":30794,"tokens_out":4219,"would_cite":false,"duration_ms":44315,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["18N10","18G30","55U35"],"pacs":[],"model":"deepseek-v4-flash","headline":"In any higher equipment, homotopy colimits are double colimits of companion diagrams.","keywords":["simplicial categories","double categories","equipments","double colimits","homotopy colimits","simplicially enriched categories","companions","higher mapping cylinders"],"falsifier":"For a specific boundary datum in sSet^♯, say an n=2 datum with three face collages Y0, Y1, Y2 glued along common edges, form the pushout Y = X ⊔_{∂X} Y• and check whether the three faces of the resulting map Y → $Δ^{2}$ are the specified Y_i up to the natural isomorphism the paper allows. If any face comes out with extra identifications or the induced map fails the universal property, the equipment property—and with it Theorem 4—fails in the main example.","tokens_in":29731,"feed_emoji":"🔺","tokens_out":6949,"duration_ms":63592,"temperature":0.7,"pith_summary":"This paper is trying to show that simplicial categories—simplicial objects in the category of categories—are two-fold categorical structures in their own right, and that their double category theory is homotopically meaningful. The central claim is Theorem 4: for any higher equipment E, indexing category J, and functor F : J → E0, the double colimit of the diagram F* obtained by composing F with the companion construction is isomorphic to the homotopy colimit of F computed in the vertical simplicially enriched category Ev. If true, this gives homotopy colimits a clean universal property of the kind double categories provide, without requiring a model structure. It also unifies two worlds usually treated separately: double-category tools for bimodules and profunctors, and simplicially enriched tools for homotopy limits and colimits.","feed_headline":"Homotopy colimits are double colimits in higher equipments","feed_subtitle":"Simplicial categories carry enough two-fold structure to give homotopy colimits a clean universal property.","key_machinery":"The equipment property is the load-bearing mechanism: for x ∈ E_n, any coherent family f_i : d_i x → y_i in E_{n-1} with matching faces extends universally to f : x → y in E_n with d_i y = y_i and d_i f = f_i. The companion construction σ* = s^n x_0(φ_{d_n σ}, ..., φ_{d_0 σ}) recursively fills the cylinder over x0 along the faces, and the tower representation expresses σ* as a composition of universal extensions. The vertical sSet-category Ev, with mapping spaces E_v(x,y)_n = E_n($s_0^{{(n)}}$x, $s_0^{{(n)}}$y), is the bridge that turns double colimits into homotopy colimits.","core_discovery":"Simplicial categories, functors E : Δ^op → Cat, are presented as two-fold structures: objects of E0 are objects, maps of E0 are vertical arrows, objects of En are horizontal n-simplices, and morphisms in En are bisimplices. The paper defines an equipment property for such E: every map from the boundary ∂x of an n-simplex x to a compatible family y• extends universally to a map x → y whose faces are exactly y•. Using this property it constructs a companion σ* for each vertical n-simplex σ = (x0 → ... → xn), built recursively as a universal extension of the companions of its faces; in sSet^♯, where E_n = sSet/Δ^n, the companion is the homotopy colimit of the chain, i.e. its higher mapping cylinder. The vertical direction Ev is a simplicially enriched category, and the main result is that the double colimit of F* equals the homotopy colimit of F in Ev.","pith_inferences":["If the equipment property holds coherently for sSet^♯, then every homotopy colimit of simplicial sets can be computed as a colimit of cotabulators, suggesting a purely categorical account of the homotopy colimit that avoids coend formulas.","The paper's note that the axioms do not force invertible comparison maps for degeneracies leaves a natural test: find a higher equipment where the comparison fails to be an isomorphism, which would delimit how close the companion construction is to a strict functor.","One could test the same double-colimit machinery on diagrams indexed by arbitrary simplicial sets rather than ordinary categories, potentially defining homotopy colimits for a wider class of indexing shapes."],"forward_implications":["In any higher equipment, the homotopy colimit of F : J → E0 in Ev is representable as a double colimit, so it inherits the unique-morphism universal property of double colimits.","For sSet^♯, the companion of a chain is the higher mapping cylinder, so the homotopy colimit of a diagram of spaces is assembled by gluing mapping cylinders of its simplices, now with a universal property.","Because Theorem 3 shows Ev is cotensored when E has double colimits, the double-colimit structure supplies tensors K ⊙ x = dcolim K_x for every simplicial set K.","The dual right-equipment property gives homotopy limits as double limits, so the same framework covers limits by reversing arrows.","The theorem generalizes the earlier result that the Grothendieck construction of a diagram of categories is the double colimit of its companion profunctors."],"supporting_citations":[{"why":"Supplies the double-category theory of limits and colimits, including cotabulators, that the paper adapts to simplicial categories.","marker":"[GP99]"},{"why":"Supplies the theory of equipments, companions, and cojoints that the higher equipment property generalizes.","marker":"[Shu08]"},{"why":"Supplies the definition of homotopy limits and colimits in simplicially enriched categories that Theorem 4 compares to double colimits.","marker":"[Shu06]"},{"why":"Supplies the simplicial combinatorics, including the boundary-correspondence proposition used to phrase the equipment property.","marker":"[GJ09]"},{"why":"Supplies the simplicially enriched category background, including the adjunction between simplicial categories and sSet-categories used to form Ev.","marker":"[Rie14]"}],"fun_headline_variants":["Double colimits in higher equipments yield homotopy colimits","Simplicial categories: double categories for homotopy","Higher equipments make homotopy colimits double","When simplicial categories act like double categories: homotopy colimits","Double colimits compute homotopy colimits in higher equipments"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"Everything rests on the claim that the pushout construction in examples like sSet^♯ really satisfies the equipment property—that filling a simplex boundary by pushout produces an object over Δ^n whose faces are exactly the specified ones and whose universal property is the stated one; the paper asserts this with a one-line diagram rather than verifying the simplicial identities and coherence.","fun_headline_variants_meta":{"raw":{"variants":["Double colimits in higher equipments yield homotopy colimits","Simplicial categories: double categories for homotopy","Higher equipments make homotopy colimits double","When simplicial categories act like double categories: homotopy colimits","Double colimits compute homotopy colimits in higher equipments"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000511,"raw_usage":{"total_tokens":2473,"prompt_tokens":923,"completion_tokens":1550,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":539,"completion_tokens_details":{"reasoning_tokens":1456}},"tokens_in":539,"tokens_out":1550,"duration_ms":12030,"temperature":1.0,"reasoning_tokens":1456,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T12:53:47.888602+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"For a specific boundary datum in sSet^♯, say an n=2 datum with three face collages Y0, Y1, Y2 glued along common edges, form the pushout Y = X ⊔_{∂X} Y• and check whether the three faces of the resulting map Y → $Δ^{2}$ are the specified Y_i up to the natural isomorphism the paper allows. If any face comes out with extra identifications or the induced map fails the universal property, the equipment property—and with it Theorem 4—fails in the main example.","supporting_citations":[],"review_version":1}