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 two 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.
The Grothendieck Computability Model
Petrakis, Iosif
2025-01-01
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 two 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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
