Logo Logo
Hilfe
Hilfe
Switch Language to English

Gambarte, Luis und Petrakis, Iosif (2025): The Grothendieck computability model. In: Theoretical Computer Science, Bd. 1057, 115550 [PDF, 2MB]

Abstract

Translating notions and results from category theory to the theory of computability models of Longley and Normann, we introduce the Grothendieck computability model. We define the first-projection-simulation and prove its basic properties. With the Grothendieck computability model, the category of computability models is shown to be a type-category, in the sense of Pitts, a result that bridges the categorical interpretation of dependent types with the theory of computability models. We also show that the category of computability models is a category with 2-family arrows and a corresponding structure of Sigma-objects. Finally, we introduce the notion of a fibration and opfibration-simulation, and we prove that the first-projection-simulation is a split opfibration-simulation.

Dokument bearbeiten Dokument bearbeiten