The Grothendieck computability model

Gambarte, Luis und Petrakis, Iosif (2025): The Grothendieck computability model. In: Theoretical Computer Science, Vol. 1057, 115550

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.

• Item Type: Journal article
• Faculties: Mathematics, Computer Science and Statistics > Mathematics
• Subjects: 500 Science > 510 Mathematics
• ISSN: 03043975
• Language: English