Grothendieck 构造的单值闭合：通过 Σ-可追溯单值结构与 Dialectica 公式

我们考察了索引范畴 $\mathsf{L} \colon \mathsf{C}^{op} \to \mathsf{CAT}$ 的 Grothendieck 构造 $\Sigma_{\mathsf{C}}\mathsf{L}$ 的范畴结构。我们的分析从 fibred limits、colimits 和单值（闭合）结构的刻画开始。对 fibred colimits 的研究自然引出了对 CHAD 中为 Expressive Total Languages 引入的 extensive indexed category 概念的推广，形成了 left Kan extensivity 概念，这为计算 Grothendieck 构造中的 colimits 提供了统一框架。随后，我们在 sufficient conditions 下建立了总范畴 $\Sigma_{\mathsf{C}}\mathsf{L}$ 的（非 fibred）单值闭合。这扩展了 G"odel 的 Dialectica 解读，基于一种新的 Σ-可追溯单值结构概念。在此概念下，Σ-可追溯的 coproducts 统一并扩展了 cocartesian coclosed 结构、biproducts 和 extensive coproducts。最后，我们考虑诱导的闭合结构是否为 fibred 的情况，指出即便存在 fibred 单值结构， induced closed structure 也不必为 fibred。