Monoidal closure of Grothendieck constructions via $\Sigma$-tractable monoidal structures and Dialectica formulas
<|reference_start|>Monoidal closure of Grothendieck constructions via $\Sigma$-tractable monoidal structures and Dialectica formulas: We study the categorical structure of the Grothendieck construction of an indexed category $\mathcal{L}:\mathcal{C}^{op}\to\mathbf{CAT}$ and characterise fibred limits, colimits, and monoidal structures. Next, we give sufficient conditions for the monoidal closure of the total category $\Sigma_\mathcal{C} \mathcal{L}$ of a Grothendieck construction of an indexed category $\mathcal{L}:\mathcal{C}^{op}\to\mathbf{CAT}$. Our analysis is a generalization of G\"odel's Dialectica interpretation, and it relies on a novel notion of $\Sigma$-tractable monoidal structure. As we will see, $\Sigma$-tractable coproducts simultaneously generalize cocartesian coclosed structures, biproducts and extensive coproducts. We analyse when the closed structure is fibred -- usually it is not.<|reference_end|>
@article{nunes2024monoidal,
    title={Monoidal closure of Grothendieck constructions via $\Sigma$-tractable
  monoidal structures and Dialectica formulas},
    author={Fernando Lucatelli Nunes and Matthijs V'ak'ar},
    journal={arXiv preprint arXiv:2405.07724},
    year={2024},
    archivePrefix={arXiv},
    eprint={2405.07724},
    primaryClass={math.CT cs.LO cs.PL}
}