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 2-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.

Bishop's measure theory (BMT) is an abstraction of the measure theory of a locally compact metric space $X$, and the use of an informal notion of a set-indexed family of complemented subsets is crucial to its predicative character. The more general Bishop-Cheng measure theory (BCMT) is a constructive version of the classical Daniell approach to measure and integration, and highly impredicative, as many of its fundamental notions, such as the integration space of $p$-integrable functions $L^p$, rely on quantification over proper classes (from the constructive point of view). In this paper we introduce the notions of a pre-measure and pre-integration space, a predicative variation of the Bishop-Cheng notion of a measure space and of an integration space, respectively. Working within Bishop Set Theory (BST), and using the theory of set-indexed families of complemented subsets and set-indexed families of real-valued partial functions within BST, we apply the implicit, predicative spirit of BMT to BCMT. As a first example, we present the pre-measure space of complemented detachable subsets of a set $X$ with the Dirac-measure, concentrated at a single point. Furthermore, we translate in our predicative framework the non-trivial, Bishop-Cheng construction of an integration space from a given measure space, showing that a pre-measure space induces the pre-integration space of simple functions associated to it. Finally, a predicative construction of the canonically integrable functions $L^1$, as the completion of an integration space, is included.

Abstract Generalizing slightly the notions of a strict computability model and of a simulation between them, which were elaborated by Longley and Normann (2015, Higher-Order Computability), we define canonical strict computability models over certain categories and appropriate presheaves on them. We study the canonical total computability model over a category $\mathcal {C}$ and a covariant presheaf on $\mathcal {C}$ and the canonical partial computability model over a category $\mathcal {C}$ with pullbacks and a pullback preserving, covariant presheaf on $\mathcal {C}$. These strict computability models are shown to be special cases of a strict computability model over a category $\mathcal {C}$ with a so-called base of computability and a pullback preserving, covariant presheaf on $\mathcal {C}$, connecting in this way Rosolini’s theory of dominions with the theory of computability models. All our notions and results are dualized by considering certain (contravariant) presheaves on appropriate categories.

Abstract Bishop’s presentation of his informal system of constructive mathematics BISH was on purpose closer to the proof-irrelevance of classical mathematics, although a form of proof-relevance was evident in the use of several notions of moduli (of convergence, of uniform continuity, of uniform differentiability, etc.). Focusing on membership and equality conditions for sets given by appropriate existential formulas, we define certain families of proof sets that provide a BHK-interpretation of formulas that correspond to the standard atomic formulas of a first-order theory, within Bishop set theory $(\mathrm{BST})$ , our minimal extension of Bishop’s theory of sets. With the machinery of the general theory of families of sets, this BHK-interpretation within BST is extended to complex formulas. Consequently, we can associate to many formulas $\phi$ of BISH a set ${\texttt{Prf}}(\phi)$ of “proofs” or witnesses of $\phi$ . Abstracting from several examples of totalities in BISH, we define the notion of a set with a proof-relevant equality, and of a Martin-Löf set, a special case of the former, the equality of which corresponds to the identity type of a type in intensional Martin-Löf type theory $(\mathrm{MLTT})$ . Through the concepts and results of BST notions and facts of MLTT and its extensions (either with the axiom of function extensionality or with Vooevodsky’s axiom of univalence) can be translated into BISH. While Bishop’s theory of sets is standardly understood through its translation to MLTT, our development of BST offers a partial translation in the converse direction.

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 space. Using a formulation similar to the formulation of McShane-Whitney theorem, we show that the Lipschitz real-valued functions on a totally bounded space are uniformly dense in the set of uniformly continuous functions. Through the introduced notion of a McShane-Whitney pair we describe the constructive content of the original McShane-Whitney extension and examine how the properties of a Lipschitz function defined on the subspace of the pair extend to its McShane-Whitney extensions on the space of the pair. Similar McShane-Whitney pairs and extensions are established for H\"{o}lder functions and $\nu$-continuous functions, where $\nu$ is a modulus of continuity. A Lipschitz version of a fundamental corollary of the Hahn-Banach theorem, and the approximate McShane-Whitney theorem are shown.

Abstract We develop the basic constructive theory of embeddings of Bishop spaces in parallel to the basic classical theory of embeddings of topological spaces. The theory of Bishop spaces is a constructive approach to point-function topology and a natural constructive alternative to the classical theory of the rings of continuous functions. Our most significant result is the translation of the classical Urysohn extension theorem within the theory of Bishop spaces. The related theory of the zero sets of a Bishop topology is also included. We work within $\textrm{BISH}^{\ast }$, Bishop’s informal system of constructive mathematics $\textrm{BISH}$ equipped with inductive definitions with rules of countably many premises.

We introduce 2-compactness, a constructive function-theoretic alternative to topological compactness, based on the notions of Bishop space and Bishop morphism, which are constructive function-theoretic alternatives to topological space and continuous function, respectively. We show that the notion of Bishop morphism is reduced to uniform continuity in important cases, overcoming one of the obstacles in developing constructive general topology posed by Bishop. We prove that 2-compactness generalizes metric compactness, namely that the uniformly continuous real-valued functions on a compact metric space form a 2-compact Bishop topology. Among other properties of 2-compact Bishop spaces, the countable Tychonoff compactness theorem is proved for them. We work within BISH*, Bishop's informal system of constructive mathematics BISH equipped with inductive definitions with rules of countably many premises, a system strongly connected to Martin-Löf's Type Theory.