3 citations · 4 across the 6 of their papers we have counts for
7 papers
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…