4 citations · 12 across the 20 of their papers we have counts for
20 papers
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…
Constructive Stone representations for separated swap and Boolean algebras
Daniel Misselbeck-Wessel, Iosif Petrakis
Swap algebras generalise Bishop's complemented powerset as Boolean algebras generalise the powerset. Actually, all Boolean algebras are swap algebras. We prove constructively a Sto…
Orthocomplemented subspaces and partial projections on a Hilbert space
Iosif Petrakis
We introduce the notion of an orthocomplemented subspace of a Hilbert space H, that is, a pair of orthogonal closed subspaces of H, as a two-dimensional counterpart to the one-dime…
Coinductive well-foundedness
Iosif Petrakis
We introduce a coinductive version of the well-foundedness of N that is used in our proof within minimal logic of the constructive counterpart CLNP to the standard least number pri…
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…
Topologies of open complemented subsets
Iosif Petrakis
We introduce cs-topologies, or topologies of open complemented subsets, as a new approach to constructive topology that preserves the duality between open and closed subsets of cla…
Categories with dependent arrows
Iosif Petrakis
We present an abstract, categorical formulation of dependent functions in a fundamental manner and independently from the Sigma-construction. For that, we define first the notion o…
Strong negation in the theory of computable functionals TCF
Nils Köpp, Iosif Petrakis
We incorporate strong negation in the theory of computable functionals TCF, a common extension of Plotkin's PCF and Gödel's system , by defining simultaneously strong n…
The Role of the Fifth Postulate in the Euclidean Construction of Parallels
Iosif Petrakis
We ascribe to the Euclidean Fifth Postulate a genuine constructive role, which makes it absolutely necessary in the parallel construction. For that, we present a reconstruction of…
Sets completely separated by functions in Bishop Set Theory
Iosif Petrakis
Within Bishop Set Theory, a reconstruction of Bishop's theory of sets, we study the so-called completely separated sets, that is sets equipped with a positive notion of an inequali…
Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory
Iosif Petrakis, Max Zeuner
Bishop's measure theory (BMT) is an abstraction of the measure theory of a locally compact metric space , and the use of an informal notion of a set-indexed family of complement…
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…
Constructive Combinatorics of Dickson's Lemma
Iosif Petrakis
We study constructively the relations between the finite cases of Dickson's lemma. Although there are many constructive proofs of them, the novel aspect of our proofs is the extrac…
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…
Direct spectra of Bishop spaces and their limits
Iosif Petrakis
We apply fundamental notions of Bishop set theory (BST), an informal theory that complements Bishop's theory of sets, to the theory of Bishop spaces, a function-theoretic approach…
McShane-Whitney extensions in constructive analysis
Iosif Petrakis
Within Bishop-style constructive mathematics we study the classical McShane-Whitney theorem on the extendability of real-valued Lipschitz functions defined on a subset of a metric…