斯科伦、哥德尔与 Hilbert 纤维

Grothendieck 纤维在捕捉依赖概念方面具有基本意义，尤其在类型论和编程语言的范畴语义学中。相关实例是 Dialectica 纤维，它们推广了 G"odel 的 Dialectica 证明解释，已在最近几年中广泛研究。我们刻画了给定纤维何时为广义、依赖 Dialectica 纤维的条件，即通过依赖乘积和求和（沿给定类的显示图）完成的迭代完成。从技术角度来看，我们补充了 Hofstra 关于 Dialectica 纤维的工作，通过一种内部视角，对经典量词无自由度的范畴化。我们也推广了 Hofstra 和 Trotta 等人关于 G"odel 纤维的工作，使其适用于依赖情况，将基类别中的笛卡尔投影类替换为任意显示图。我们讨论了这如何恢复范畴逻辑和证明论中一系列相关示例。此外，作为另一个实例，我们引入了 Hilbert 纤维，提供了对 Hilbert 的 $\epsilon$- 和 $\tau$- 运算符的范畴理解，这在证明论中广为人知。