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$-tractible monoidal structure. As we will see, $\Sigma$-tractible coproducts simultaneously generalize cocartesian coclosed structures, biproducts and extensive coproducts. We analyse when the closed structure is fibred -- usually it is not.
翻译:我们研究指标范畴 $\mathcal{L}:\mathcal{C}^{op}\to\mathbf{CAT}$ 的格罗滕迪克构造的范畴结构,并刻画其纤维极限、余极限与幺半结构。随后,我们给出指标范畴 $\mathcal{L}:\mathcal{C}^{op}\to\mathbf{CAT}$ 的格罗滕迪克构造的全范畴 $\Sigma_\mathcal{C} \mathcal{L}$ 满足幺半闭性的充分条件。我们的分析是哥德尔论题解释的推广,其核心依赖于一种新颖的 $\Sigma$-可牵引幺半结构。如我们将看到的,$\Sigma$-可牵引余积同时推广了余笛卡尔余闭结构、双积与广延余积。我们进一步分析了闭结构何时是纤维的——通常这一性质并不成立。