Thomason's colimit theorem for the double category of elements

Andrew Gill; Maru Sarazola

Thomason's colimit theorem for the double category of elements

T0 review · 0 major / 6 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read 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$.

desk verdict A genuinely new double-categorical Thomason theorem, proved by a well-chosen bar construction comparison; the proof is dense but sound. read the letter →

arxiv 2506.08246 v1 pith:M7CKFVNY submitted 2025-06-09 math.CT math.AT

Andrew Gill , Maru Sarazola This is my paper · ORCID

classification math.CTmath.AT MSC 18N1018G3055U10

keywords doublecategoryofelementsThomason'scolimittheoremhomotopycolimits2-categories2-functorsbisimplicialsetsbarconstructionclassifyingspaces

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

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$.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

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.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the 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.

What 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.

Soft 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.

Verdict: 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.

Referee Report

0 major / 6 minor

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.

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.

minor comments (6)

[Eq. (7)] 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.
[Eq. (12)] 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.
[Theorem 3.7] 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.
[Example 3.5] 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).
[Proof of Theorem 3.1] 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.
[Definitions 3.2 and 3.3] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the main proof reduces to an explicit bar-construction isomorphism and appeals only to independent external theorems.

full rationale

The paper proves Theorem 3.1 by combining the external Theorem B ([Ceg11, Theorem 4.5(i)]) with a direct comparison of bar constructions: it constructs explicit inverse simplicial isomorphisms Φ and Θ between WN∫F and WN∫∫F (proof of Theorem 3.1, Eqs. (12)–(13)) and verifies that Θ respects faces and degeneracies. This comparison is substantive rather than definitional; Section 3.1 documents why the naive bisimplicial nerve maps fail, and the face/degeneracy checks in Eqs. (14)–(17) are nontrivial. The only self-cited prior work, [MSV23], appears in the introduction as background context and does not support any step of the derivation. The load-bearing external results, [CR05, Theorem 1.1] and [Ceg11, Theorem 4.5(i)], are independent, parameter-free theorems about arbitrary bisimplicial sets and 2-functors, respectively, and they are not derived from or assumed by the present paper. The minor typo in Eq. (7) is a presentational issue, not circularity. No step reduces by construction to its own input, so the honest finding is no significant circularity.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The central claim rests on no fitted parameters and no invented entities. It relies on standard external theorems (Cegarra for the 2-category of elements, Cegarra-Remedios for the bar construction) and on the stated strictness convention. These are legitimate background assumptions, not circular moves.

assumptions (4)

domain assumption All 2-categories, 2-functors, and double categories are strict, and F is a strict 2-functor.
The Conventions section restricts the theorem to strict structures. Pseudo and lax variants are not addressed.
standard math Cegarra's Theorem B: B hocolim F ≃ B(∫_C F) for the 2-category of elements.
Used at the start of Section 3 to reduce Theorem 3.1 to comparing B(∫F) with B(∬F).
standard math Cegarra-Remedios Theorem 3.7: every bisimplicial set is naturally weakly equivalent to its bar construction WX.
Used to translate the isomorphism of bar constructions into a homotopy equivalence of the associated spaces.
standard math The diagonal realization of a bisimplicial set and the iterated realizations in each direction are homotopy equivalent.
Invoked in Remark 2.5 and Section 3.1 to identify the spatial models for 2-categories and double categories.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Thomason's colimit theorem for the double category of elements." pith.science (2026). https://pith.science/paper/M7CKFVNY

@misc{pith2026250608246,
  author       = {Pith},
  title        = {Pith review of: Thomason's colimit theorem for the double category of elements},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/M7CKFVNY}},
  note         = {Machine review of arXiv:2506.08246}
}

abstract

We show that, for any 2-category $C$ and 2-functor $F\colon C \to Cat$, the double category of elements $\iint_C F$ introduced by Grandis and Par\'e satisfies a version of Thomason's colimit theorem; that is, there is a weak homotopy equivalence $B hocolim F\simeq B(\iint_C F)$.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

19 extracted references · 18 canonical work pages

[1]

Grothendieck construction for bicategories

Igor Bakovic. Grothendieck construction for bicategories. http://www. irb. hr/korisnici/ibakovic/sgc. pdf, 2009

work page 2009
[2]

Fibred 2-categories and bicategories

Mitchell Buckley. Fibred 2-categories and bicategories. J. Pure Appl. Algebra , 218(6):1034--1074, 2014

work page 2014
[3]

Calvo, A

M. Calvo, A. M. Cegarra, and B. A. Heredia. Bicategorical homotopy fiber sequences. J. Homotopy Relat. Struct. , 9(1):125--173, 2014

work page 2014
[4]

A. M. Cegarra. Homotopy fiber sequences induced by 2-functors. J. Pure Appl. Algebra , 215(4):310--334, 2011

work page 2011
[5]

A. M. Cegarra and B. A. Heredia. Homotopy colimits of 2-functors. J. Homotopy Relat. Struct. , 11(4):735--774, 2016

work page 2016
[6]

2-limits and 2-terminal objects are too different

tslil clingman and Lyne Moser. 2-limits and 2-terminal objects are too different. Appl. Categ. Structures , 30(6):1283--1304, 2022

work page 2022
[7]

Bi-initial objects and bi-representations are not so different

tslil clingman and Lyne Moser. Bi-initial objects and bi-representations are not so different. Cah. Topol. G\' e om. Diff\' e r. Cat\' e g. , 63(3):259--330, 2022

work page 2022
[8]

A. M. Cegarra and Josu\'e Remedios. The relationship between the diagonal and the bar constructions on a bisimplicial set. Topology Appl. , 153(1):21--51, 2005

work page 2005

Show all 19 references

[9]

auser Classics. Birkh\

Paul G. Goerss and John F. Jardine. Simplicial homotopy theory . Modern Birkh\"auser Classics. Birkh\"auser Verlag, Basel, 2009. Reprint of the 1999 edition [MR1711612]

2009
[10]

Limits in double categories

Marco Grandis and Robert Paré. Limits in double categories. Cahiers Topologie G\' e om. Diff\' e rentielle Cat\' e g. , 40(3):162--220, 1999

1999
[11]

Persistent double limits and flexible weighted limits

Marco Grandis and Robert Par\' e . Persistent double limits and flexible weighted limits. https://www.mscs.dal.ca/ pare/DblPrs2.pdf, 2019

2019
[12]

Higher dimensional categories

Marco Grandis. Higher dimensional categories . World Scientific Publishing Co. Pte. Ltd., Hackensack, NJ, 2020. From double to multiple categories

2020
[13]

V. A. Hinich and V. V. Schechtman. Geometry of a category of complexes and algebraic K -theory. Duke Math. J. , 52(2):399--430, 1985

1985
[14]

2-dimensional categories

Niles Johnson and Donald Yau. 2-dimensional categories . Oxford University Press, Oxford, 2021

2021
[15]

Discrete 2-fibrations

Michael Lambert. Discrete 2-fibrations. High. Struct. , 8(1):54--96, 2024

2024
[16]

Internal G rothendieck construction for enriched categories

Lyne Moser, Maru Sarazola, and Paula Verdugo. Internal G rothendieck construction for enriched categories. arXiv:2308.14455, 2023

2023 arXiv
[17]

Category theory in context

Emily Riehl. Category theory in context . Aurora Modern Math Originals. Dover Publications, 2016

2016
[18]

R. W. Thomason. Homotopy colimits in the category of small categories. Math. Proc. Cambridge Philos. Soc. , 85(1):91--109, 1979

1979
[19]

Enriched categories, internal categories and change of base

Dominic Verity. Enriched categories, internal categories and change of base. Repr. Theory Appl. Categ. , (20):1--266, 2011

2011

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.

[1] [1]

Grothendieck construction for bicategories

Igor Bakovic. Grothendieck construction for bicategories. http://www. irb. hr/korisnici/ibakovic/sgc. pdf, 2009

work page 2009

[2] [2]

Fibred 2-categories and bicategories

Mitchell Buckley. Fibred 2-categories and bicategories. J. Pure Appl. Algebra , 218(6):1034--1074, 2014

work page 2014

[3] [3]

Calvo, A

M. Calvo, A. M. Cegarra, and B. A. Heredia. Bicategorical homotopy fiber sequences. J. Homotopy Relat. Struct. , 9(1):125--173, 2014

work page 2014

[4] [4]

A. M. Cegarra. Homotopy fiber sequences induced by 2-functors. J. Pure Appl. Algebra , 215(4):310--334, 2011

work page 2011

[5] [5]

A. M. Cegarra and B. A. Heredia. Homotopy colimits of 2-functors. J. Homotopy Relat. Struct. , 11(4):735--774, 2016

work page 2016

[6] [6]

2-limits and 2-terminal objects are too different

tslil clingman and Lyne Moser. 2-limits and 2-terminal objects are too different. Appl. Categ. Structures , 30(6):1283--1304, 2022

work page 2022

[7] [7]

Bi-initial objects and bi-representations are not so different

tslil clingman and Lyne Moser. Bi-initial objects and bi-representations are not so different. Cah. Topol. G\' e om. Diff\' e r. Cat\' e g. , 63(3):259--330, 2022

work page 2022

[8] [8]

A. M. Cegarra and Josu\'e Remedios. The relationship between the diagonal and the bar constructions on a bisimplicial set. Topology Appl. , 153(1):21--51, 2005

work page 2005