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

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