Monoidal closure of Grothendieck constructions via $Σ$-tractable monoidal structures and Dialectica formulas
Fernando Lucatelli Nunes, Matthijs Vákár
TL;DR
This work analyzes the total category $\\Sigma_\\mathcal{C} \,\\mathcal{L}$ of an indexed category $\\mathcal{L}: \\mathcal{C}^{op}\to \\mathbf{CAT}$, focusing on limits, colimits, and monoidal closure. It introduces $\\Sigma$-tractable monoidal structures and a Dialectica-style formula to guarantee monoidal closure, even in non-fibred cases, while linking to dependent type theory via $\\Pi$-types and strong $\\Sigma$-types. By establishing necessary and sufficient conditions for fibred and non-fibred closure, the paper unifies extensive, cartesian, and biproduct contexts and provides broad applicability through examples like $\\mathbf{Fam}(\\mathcal{D})$ and lax comma constructions. It also extends Gödel's Dialectica interpretation to the Grothendieck setting, offering a principled approach to exponentials in a wide class of indexed monoidal categories. The results have implications for higher-order containers, CHAD, and dependently typed semantics, with potential impact on programming language theory and categorical logic.
Abstract
We examine the categorical structure of the Grothendieck construction $Σ_{\mathsf{C}}\mathsf{L}$ of an indexed category $\mathsf{L} \colon \mathsf{C}^{op} \to \mathsf{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 $Σ_{\mathsf{C}}\mathsf{L}$. 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.