{"id":"6aa3126b-4e2e-46b2-a5c7-e7c1f38c4467","arxiv_id":"2506.08246","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"The double category of elements of a 2-functor is weakly homotopy equivalent to the homotopy colimit of that 2-functor.","lead":"For any 2-category C and 2-functor F into categories, the double category of elements built from F has the same homotopy type as the homotopy colimit of F. This extends Thomason's classical colimit theorem to a double-categorical construction used for representability and weighted limits.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified; the proof's bijection and external references appear sound.","rationale":"The stress-test pass focused on the internal combinatorics of the bijection Φ: WN∫F ⇄ WN∫∫F, since this is where a silent error would invalidate the proof. I re-derived the data in Eq (7) and Eq (9), checked the inverse property (ΘΦ = id and ΦΘ = id) using the determinacy relations Eq (8), Eq (10), Eq (11), and verified the face and degeneracy calculations. The composition equality in the face-map check (m = p−i+1) uses exactly the square relation, and the degeneracy equality relies on (id_c, e_x) = id_{(c,x)}, both correct. The only discovered defect is a typo in the stated type of α^n_m in Eq (7); the subsequent formulas use the correct relation. The two external theorems (Cegarra–Remedios and Cegarra) are standard, with the stated hypotheses covering the bisimplicial nerves and 2-functors used here. Consequently, no change to the reader's ACCEPT verdict is warranted.","tokens_in":13869,"tokens_out":22926,"duration_ms":202561,"concrete_test":"Implement the definitions of WN∫F and WN∫∫F for a small 2-category (e.g., the one in Example 2.3) and computationally verify for p ≤ 4 that Φ_p and Θ_p are inverse and satisfy the simplicial identities; this would catch any hidden indexing error in the face/degeneracy verification.","verdict_should_be":"UNCHANGED","load_bearing_attack":"I find no load-bearing flaw in the central argument. The proof of Theorem 3.1 reduces to showing WN∫F ≅ WN∫∫F and then appeals to Cegarra–Remedios' theorem. The levelwise bijection Φ/Θ is carefully constructed; I checked the inverse verification and the face/degeneracy checks, and the only notable issue is a typo in Eq (7) in the type of the 2-cell α^n_m, which should read α^n_m : (f^{n+1}_m, φ^{n+1}_m) ⇒ (f^n_m, φ^n_m) to be consistent with the relation φ^n_m = (Fα^n_m)_{x_{m−1}} ∘ φ^{n+1}_m. This typo does not affect the formulas that follow. The reliance on [CR05, Theorem 1.1] and [Ceg11, Theorem 4.5(i)] is standard and appropriate; both results are well-established for arbitrary bisimplicial sets and 2-functors respectively. Thus no load-bearing concern is identified.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proves Theorem 3.1: for any strict 2-category C and strict 2-functor F:C^op -> Cat, the double category of elements \\iint_C F of Grandis and Paré satisfies Thomason's colimit theorem, i.e. B hocolim F is weakly equivalent to B(\\iint_C F). The proof combines Cegarra's Theorem B for the 2-category of elements with a new comparison between the homotopy types of \\int_C F and \\iint_C F. The comparison is effected by an explicit levelwise isomorphism between the bar constructions of the bisimplicial nerves of the two objects, and then by the Cegarra-Remedios theorem relating the diagonal and bar construction.","tokens_in":14013,"tokens_out":16979,"duration_ms":188854,"significance":"The result is a natural and useful homotopy-theoretic companion to the categorical results already established for the double category of elements: it shows that the double-categorical replacement, which fixes representability and weighted-limit behavior, does not lose the homotopy colimit interpretation. The proof is direct and constructive, and it does not assume the statement being proved; its main ingredients are two established external theorems, Cegarra's Theorem B and the Cegarra-Remedios comparison. The levelwise bijection is explicit, and the paper includes helpful examples, including a documented failed attempt that motivates the choice of the bar construction. I regard the central claim as sound.","major_comments":[],"minor_comments":[{"comment":"The type of the 2-cell α^n_m is misprinted: it should read α^n_m : (f^{n+1}_m, φ^{n+1}_m) ⇒ (f^n_m, φ^n_m), consistent with the displayed relation φ^n_m = (Fα^n_m)_{x_{m-1}} ∘ φ^{n+1}_m. As printed, the second components do not match the relation.","section":"Eq. (7)"},{"comment":"In the object formula for Φ_p and in the formula for the vertical morphisms, the symbols x^n and x^{n+1} should be x_n and x_{n+1} (the input objects of Eq. (7)); otherwise the definition refers to data not present in the input.","section":"Eq. (12)"},{"comment":"The statement 'X → WX' should clarify that the weak equivalence is between the diagonal of the bisimplicial set X and its bar construction WX (or equivalently that X is identified with its diagonal). As written, the domain is bisimplicial and the codomain is simplicial.","section":"Theorem 3.7"},{"comment":"In the paragraph introducing the attempted inverse map, the codomain of Θ is written as ∫_C F; it should be the bisimplicial nerve N∫_C F (or the appropriate simplicial set).","section":"Example 3.5"},{"comment":"The verifications that Θ_pΦ_p = id and that Φ_pΘ_p = id are compressed into 'straightforward' and 'not hard to see' after Eq. (13). Since these are load-bearing steps in a notation-heavy proof, a worked representative case for each composite would improve readability and verifiability.","section":"Proof of Theorem 3.1"},{"comment":"The (m,n)-simplices of the two bisimplicial nerves are described by schematic pasting diagrams only; a sentence giving the precise orientational convention, indicating which direction is m and which is n, would remove ambiguity, especially because the bar construction mixes the two directions.","section":"Definitions 3.2 and 3.3"}],"recommendation":"minor_revision","confidential_remarks":null},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper proves that Grandis–Paré's double category of elements satisfies Thomason's colimit theorem: for any 2-category C and 2-functor F: C^op → Cat, there's a weak homotopy equivalence B hocolim F ≃ B(∬_C F). That result is new, and the proof is not a routine translation. A naive comparison of bisimplicial nerves fails, and the authors correctly identify the bar construction as the right model, then produce an explicit simplicial isomorphism between WN∫F and WN∬F. That's the core original work, and it holds together.\n\nWhat the paper does well: it's honest about the failed attempts, which makes the chosen model much easier to trust. The background is appropriately concise, and the citation pattern is clean—Cegarra's 2-categorical Thomason theorem and Cegarra–Remedios on bar constructions are the right external anchors, and the self-citation to [MSV23] is only contextual. The categorical motivation (representability and weighted limits encoded by the double category of elements) is well summarized.\n\nSoft spots: the proof is notationally brutal. Several verification steps are waved at with 'straightforward' or 'not hard'—the inverse check after Eq. (13) and parts of the degeneracy comparison being the main ones. A referee will need to do real work to confirm those, and the authors could make life easier by expanding at least one of them. There's also a small typo in Eq. (7): the 2-cell α^n_m should have codomain (f^n_m, φ^{n+1}_m), not (f^n_m, φ^n_m), to be consistent with the relation that follows. It doesn't affect the rest. The reliance on [CR05, Theorem 1.1] is load-bearing but standard, and not a concern.\n\nVerdict: this is a solid, citable contribution for anyone working on double categories and homotopy coherent constructions. It deserves a serious referee. I'd send it to peer review, and ask the authors to expand the compressed verifications.","headline":"A genuinely new double-categorical Thomason theorem, proved by a well-chosen bar construction comparison; the proof is dense but sound.","tokens_in":14553,"tokens_out":2296,"would_cite":true,"duration_ms":24611,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["18N10","18G30","55U10"],"pacs":[],"model":"deepseek-v4-flash","headline":"For any 2-category $C^{\\mathrm{op}}$ and 2-functor $F\\colon C^{\\mathrm{op}}\\to\\mathbf{Cat}$, the double category of elements $\\iint_C F$ is weakly homotopy equivalent to the homotopy colimit of $F$.","keywords":["double category of elements","Thomason's colimit theorem","homotopy colimits","2-categories","2-functors","bisimplicial sets","bar construction","classifying spaces"],"falsifier":"Take a 2-functor out of the walking 2-category (one object, one non-identity 2-cell) and compute the fundamental group of the classifying spaces of its 2-category of elements and its double category of elements; differing groups would refute the theorem. A more mechanical check is to verify the claimed simplicial isomorphism $\\Theta$ on a single 3-simplex: any failure to commute with a face or degeneracy map would break the proof.","tokens_in":13636,"feed_emoji":"🧩","tokens_out":9859,"duration_ms":100409,"temperature":0.7,"pith_summary":"This paper proves that the double category of elements of a 2-functor into Cat carries the correct homotopy type: its classifying space is weakly homotopy equivalent to the 2-functor's homotopy colimit. This extends Thomason's colimit theorem, which gives the same result for the ordinary (2-)category of elements, to the double-categorical setting. The proof works by showing that the double category of elements and the 2-category of elements are always homotopy equivalent, via an explicit isomorphism between the bar constructions of their bisimplicial nerves. The result matters because the double category of elements is already known to be the right categorical tool for representability and weighted limits, so it can now serve as a homotopically faithful model as well.","feed_headline":"Double category of elements computes homotopy colimits","feed_subtitle":"Extends Thomason's theorem to the double-categorical setting, matching the 2-category of elements up to homotopy.","key_machinery":"The bar construction of a bisimplicial set is the operative tool: for a bisimplicial set $X$, the $k$-simplices of $WX$ are tuples $(t_0,\\dots,t_k)$ with $t_j\\in X_{j,k-j}$ satisfying $d^v_0 t_j = d^h_{j+1}t_{j+1}$, with the evident face and degeneracy maps. The paper gives a bisimplicial nerve for a 2-category (whose $(m,n)$-simplices are pastings with $m$ horizontal and $n$ vertical arrows) and for a double category (whose $(m,n)$-simplices are $m\\times n$ grids of squares), then proves that $W N\\int_C F$ and $W N\\iint_C F$ are isomorphic simplicial sets. The isomorphism $\\Phi$ (with inverse $\\Theta$) reassembles a simplex of the 2-category-of-elements nerve into the 'corners' that appear in the double-category nerve, and the bar construction conditions make the reassembly compatible with faces and degeneracies. This comparison is the load-bearing mechanism that turns the categorical data of the two elements constructions into the same homotopy type.","core_discovery":"The central claim is Theorem 3.1: for any strict 2-category $C$ and strict 2-functor $F\\colon C^{\\mathrm{op}}\\to\\mathbf{Cat}$, there is a weak homotopy equivalence $B\\,\\mathrm{hocolim}\\,F \\simeq B(\\iint_C F)$, where $\\iint_C F$ is Grandis and Par\\'e's double category of elements. Since Cegarra's theorem already identifies $B\\,\\mathrm{hocolim}\\,F$ with $B(\\int_C F)$ for the 2-category of elements, the heart of the paper is a proof that $B(\\int_C F)\\simeq B(\\iint_C F)$. The authors construct this equivalence by defining bisimplicial nerves for 2-categories and for double categories, applying the bar construction $W$ to each, and exhibiting inverse simplicial maps that identify $W N\\int_C F$ with $W N\\iint_C F$ levelwise. This shows the two constructions encode the same combinatorial data once the two-dimensional information is flattened, so their classifying spaces are weakly equivalent.","pith_inferences":["The inverse isomorphisms $\\Phi,\\Theta$ appear natural in $F$, so the equivalence likely upgrades to a natural weak equivalence and makes $B\\iint_C$ a functorial model for homotopy colimits of 2-functors.","A similar bar-construction comparison might resolve the analogous question for lax or pseudo versions of the elements construction, where the naive nerve maps also fail.","One could test whether the equivalence passes through the geometric realization of the diagonal nerve directly, which would give a shorter route to Theorem 3.1 without invoking Theorem 3.7."],"forward_implications":["For every strict 2-functor $F\\colon C^{\\mathrm{op}}\\to\\mathbf{Cat}$, the double category of elements $\\iint_C F$ is a valid model for the homotopy colimit of $F$.","The classifying spaces $B(\\int_C F)$ and $B(\\iint_C F)$ are weakly equivalent, so homotopy invariants of either construction coincide for all such $F$.","The comparison is realized by an explicit isomorphism of simplicial sets between two bar constructions, making the equivalence constructive and checkable simplex by simplex.","Since prior categorical results show $\\iint_C F$ encodes representability and double limits, those double-categorical tools can be used on an object whose homotopy type is the homotopy colimit of $F$."],"supporting_citations":[{"why":"Supplies the bar-construction weak equivalence $X \\simeq WX$ used to turn the levelwise bijection into a homotopy equivalence.","marker":"[CR05, Theorem 1.1]"},{"why":"Establishes Thomason's theorem for the 2-category of elements $\\int_C F$, reducing the main theorem to comparing $\\int_C F$ and $\\iint_C F$.","marker":"[Ceg11, Theorem 4.5(i)]"},{"why":"The classical Thomason theorem for $\\mathbf{Cat}$-valued functors that the paper extends to the double-categorical setting.","marker":"[Tho79, Theorem 1.2]"},{"why":"Introduces the double category of elements $\\iint_C F$, the construction whose homotopy type is the subject of the theorem.","marker":"[GP19, §1.2]"},{"why":"Defines the homotopy colimit of a 2-functor, the space the theorem compares with $B(\\iint_C F)$.","marker":"[HS85, Definition 2.2.2]"}],"fun_headline_variants":["Double category of elements models homotopy colimits","Double category of elements gets Thomason's theorem","Thomason colimit theorem for double categories of elements","Homotopy colimits via double category of elements","Extending Thomason to double categories"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The proof relies, without proving it, on the theorem that any bisimplicial set is naturally weakly homotopy equivalent to its bar construction; if that theorem were false for the specific nerves used here, the claimed equality of homotopy types would not follow.","fun_headline_variants_meta":{"raw":{"variants":["Double category of elements models homotopy colimits","Double category of elements gets Thomason's theorem","Thomason colimit theorem for double categories of elements","Homotopy colimits via double category of elements","Extending Thomason to double categories"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000306,"raw_usage":{"total_tokens":1696,"prompt_tokens":833,"completion_tokens":863,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":449,"completion_tokens_details":{"reasoning_tokens":789}},"tokens_in":449,"tokens_out":863,"duration_ms":8991,"temperature":1.0,"reasoning_tokens":789,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T05:16:40.038110+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a 2-functor out of the walking 2-category (one object, one non-identity 2-cell) and compute the fundamental group of the classifying spaces of its 2-category of elements and its double category of elements; differing groups would refute the theorem. A more mechanical check is to verify the claimed simplicial isomorphism $\\Theta$ on a single 3-simplex: any failure to commute with a face or degeneracy map would break the proof.","supporting_citations":[],"review_version":1}