4 citations · 12 across the 20 of their papers we have counts for
5 papers · 1 filter
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…
Families of Sets in Bishop Set Theory
Iosif Petrakis
We develop the theory of set-indexed families of sets and subsets within the informal Bishop Set Theory BST, a reconstruction of Bishop's theory of sets.
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…
Closed subsets in Bishop topological groups
Iosif Petrakis
We introduce the notion of a Bishop topological group i.e., a group X equipped with a Bishop topology of functions F such that the group operations of X are Bishop morphisms with r…