Monoidal closure of Grothendieck constructions via $\Sigma$-tractable monoidal structures and Dialectica formulas

Abstract

We examine the categorical structure of the Grothendieck construction $\Sigma_{\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 $\Sigma_{\mathsf{C}}\mathsf{L}$. This extends G\"odel's Dialectica interpretation and rests upon a new notion of $\Sigma$-tractable monoidal structure. Under this notion, $\Sigma$-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.