Categories with a Base of Computability

Abstract

The notion of a base of computability $\mathcal{C}$ in a category $\mathcal{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, $\Sigma$)-category with a terminal object. Moreover, we prove that CatBaseComp is a (2-fam, $\Sigma$)-category, a 2-categorical generalisation of a (fam, $\Sigma$)-category. Finally, we describe the canonical (2-dep, $\Sigma$)-structure of CatBaseComp, i.e., the canonical dependent arrows of CatBaseComp that are compatible with its (2-fam, $\Sigma$)-structure.