We examine the categorical structure of the Grothendieck construction Σ_cL of an indexed category L: C^op → CAT. Our analysis begins with characterisations of fibred limits, colimits, and monoidal (closed) structures. The study of fibred colimits leads naturally to a generalisation of the notion of extensive indexed category introduced in CHAD for Expressive Total Languages, and gives rise to the concept of left Kan extensivity, which provides a uniform framework for computing colimits in Grothendieck constructions.
We then establish sufficient conditions for the (non-fibred) monoidal closure of the total category Σ_cL. This extends Gödel’s Dialectica interpretation, and rests upon a new notion of Σ-tractable monoidal structure. Under this notion, Σ-tractable coproducts unify and extend cocartesian coclosed structures, biproducts, and extensive coproducts. Finally, we consider when the induced closed structure is fibred, showing that this need not hold in general, even in the presence of a fibred monoidal structure.
Keywords: Grothendieck constructions, limits, colimits, exponentials, cartesian closed categories, monoidal closed categories, free coproduct completion, oplax colimits, lax comma categories, extensive indexed categories, left Kan extensive indexed categories
2020 MSC: 18N10, 18C10, 18F10, 18A22, 18A40, 18D10, 03B70, 68Q55, 03F52, 03F03
Theory and Applications of Categories, Vol. 44, 2025, No. 35, pp 1153-1217.
Published 2025-11-02.
TAC Home