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

Abstract

We study the categorical structure of the Grothendieck construction of an indexed category L:Cop→CAT and characterise fibred limits, colimits, and monoidal structures. Next, we give sufficient conditions for the monoidal closure of the total category ΣCL of a Grothendieck construction of an indexed category L:Cop→CAT. Our analysis is a generalization of Gödel's Dialectica interpretation, and it relies on a novel notion of Σ-tractable monoidal structure. As we will see, Σ-tractable coproducts simultaneously generalize cocartesian coclosed structures, biproducts and extensive coproducts. We analyse when the closed structure is fibred -- usually it is not.