The Grothendieck computability model

TL;DR

This paper introduces the Grothendieck computability model, translating category theory concepts into computability models, and establishes foundational properties and structures such as type-categories and fibrations.

Contribution

It presents the first Grothendieck computability model and the first-projection-simulation, connecting category theory with computability models in a novel way.

Findings

The Grothendieck computability model has basic properties proven.

The category of computability models forms a type-category.

First-projection-simulation is a split opfibration-simulation.

Abstract

Translating notions and results from category theory to the theory of computability models of Longley and Normann, we introduce the Grothendieck computability model and the first-projection-simulation. We prove some basic properties of the Grothendieck computability model, and we show that the category of computability models is a type-category, in the sense of Pitts. We introduce the notion of a fibration and opfibration-simulation, and we show that the first-projection-simulation is a split opfibration-simulation.