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

TL;DR

This paper explores the categorical structure of Grothendieck constructions, introducing $ ext{Sigma}$-tractable monoidal structures and extending Dialectica interpretations to establish conditions for monoidal closure.

Contribution

It provides new conditions for monoidal closure of Grothendieck constructions using $ ext{Sigma}$-tractable structures, extending Dialectica interpretations and unifying various coproduct notions.

Findings

Established sufficient conditions for monoidal closure in Grothendieck constructions.

Introduced $ ext{Sigma}$-tractable monoidal structures that unify multiple coproduct concepts.

Analyzed fibred versus non-fibred monoidal closure, showing limitations in fibred cases.

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.