AI 中文总结
本文引入具有可计算性基的范畴的范畴CatBaseComp，证明其具有所有有限极限，研究Grothendieck纤维化对可计算性基的提升与映射性质，关联依赖类型论语义并证明其相关范畴结构。
AI 中文摘要
范畴中的可计算性基$\boldsymbol{\text{Base of Computability}}\boldsymbol{\text{Base of Computability}}$是作为从范畴生成Longley-Normann意义下可计算性模型的工具引入的。本文引入了具有可计算性基的范畴的范畴$\boldsymbol{\text{CatBaseComp}}$，并证明$\boldsymbol{\text{CatBaseComp}}$具有所有有限极限。我们证明：Grothendieck纤维化可将基范畴中的可计算性基提升为纤维化总范畴中的可计算性基；反之，保持拉回的Grothendieck纤维化可将总范畴中的可计算性基映射为纤维化基范畴中的可计算性基。将$\boldsymbol{\text{CatBaseComp}}$与依赖类型论语义关联，我们证明$\boldsymbol{\text{CatBaseComp}}$是类型范畴，即带终对象的$(\text{fam}, \boldsymbol{\text{fam}})$范畴。此外，我们证明$\boldsymbol{\text{CatBaseComp}}$是$(\text{2-fam}, \boldsymbol{\text{2-fam}})$范畴，即$(\text{fam}, \boldsymbol{\text{fam}})$范畴的2范畴推广。最后，我们描述$\boldsymbol{\text{CatBaseComp}}$的典范$(\text{2-dep}, \boldsymbol{\text{2-dep}})$结构，即与其$(\text{2-fam}, \boldsymbol{\text{2-fam}})$结构兼容的$\boldsymbol{\text{CatBaseComp}}$的典范依赖箭头。
英文摘要
The notion of a base of computability $\mathscr{C}$ in a category $\mathscr{C}$ was introduced as a tool to generate computability models, in the sense of Longley and Normann, from categories. In this paper we introduce the category $\mathsf{CatBaseComp}$ of categories with a base of computability, and we show that $\mathsf{CatBaseComp}$ has all pie limits. We prove that a Grothendieck fibration lifts a base of computability in the base category to a base of computability in the total category of the fibration, and conversely, a pullback-preserving Grothendieck fibration maps a base of computability in the total category to a base of computability in the base category of the fibration. Connecting $\mathsf{CatBaseComp}$ with the semantics of dependent type theory, we show that $\mathsf{CatBaseComp}$ is a type-category, or a (fam, $Σ$)-category with a terminal object. Moreover, we prove that CatBaseComp is a (2-fam, $Σ$)-category, a 2-categorical generalisation of a (fam, $Σ$)-category. Finally, we describe the canonical (2-dep, $Σ$)-structure of CatBaseComp, i.e., the canonical dependent arrows of CatBaseComp that are compatible with its (2-fam, $Σ$)-structure.
