3 citations · 4 across the 10 of their papers we have counts for
6 papers · 1 filter
Categories with a Base of Computability
Luis Gambarte, Iosif Petrakis
The notion of a base of computability in a category was introduced as a tool to generate computability models, in the sense of Longley and Normann, from…
The Grothendieck computability model
Luis Gambarte, Iosif Petrakis
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-p…
Univalent typoids
Iosif Petrakis
A typoid is a type equipped with an equivalence relation, such that the terms of equivalence between the terms of the type satisfy certain conditions, with respect to a given equiv…
From the Sigma-type to the Grothendieck construction
Iosif Petrakis
We translate properties of the Sigma-type in Martin-Löf Type Theory (MLTT) to properties of the Grothendieck construction in category theory. Namely, equivalences in MLTT that invo…
Chu representations of categories related to constructive mathematics
Iosif Petrakis
If C is a closed symmetric monoidal category, the Chu category Chu(C, g) over C and an object g of it was defined by Chu, as a *-autonomous category generated from C. Bishop introd…
Computability models over categories
Iosif Petrakis
Generalising slightly the notions of a strict computability model and of a simulation between them, which were elaborated by Longley and Normann, we define canonical computability…