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^op 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^op. 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.