1 Core QBS Theory
In this chapter we define quasi-Borel spaces, their morphisms, and the fundamental categorical constructions: products, exponentials, coproducts, dependent products, and the unit type. We establish cartesian closure, the \(L \dashv R\) adjunction between QBS and measurable spaces, and introduce standard Borel spaces with their full faithfulness property.
The development is parametric in a realType \(R\) from math-comp analysis. We write \(\mathbb {R}\) for the carrier of \(R\) and \(m\mathbb {R}\) for its Borel measurable space.
1.1 QBS Definition
A quasi-Borel space (QBS) over \(R\) is a type \(T\) equipped with a set \(M_X \subseteq (\mathbb {R} \to T)\) of random elements satisfying three axioms:
Composition (qbs_Mx_comp): If \(\alpha \in M_X\) and \(f : \texttt{\{ mfun mR {\gt}-{\gt} mR\} }\) (a bundled measurable function), then \(\alpha \circ f \in M_X\).
Constants (qbs_Mx_const): For every \(x : T\), the constant function \(\lambda r.\; x\) is in \(M_X\).
Gluing (qbs_Mx_glue): If \(P : \texttt{\{ mfun mR {\gt}-{\gt} nat\} }\) and \(F_i \in M_X\) for all \(i\), then \(\lambda r.\; F_{P(r)}(r) \in M_X\).
The HB structure QBSpace packages this mixin with a short type name qbsType R. All type constructions (prodQ, expQ, unitQ, etc.) use the Section + HB.instance Definition pattern recommended by mathcomp maintainers.
1.2 Morphisms
A function \(f : X \to Y\) between QBS is a QBS morphism if for every \(\alpha \in M_X\), we have \(f \circ \alpha \in M_Y\).
The identity function \(\mathrm{id} : X \to X\) is a QBS morphism.
If \(f : X \to Y\) and \(g : Y \to Z\) are QBS morphisms, then \(g \circ f : X \to Z\) is a QBS morphism.
For any \(y : Y\), the constant function \(\lambda x.\; y\) is a QBS morphism.
1.3 The R Functor
The functor \(R : \mathbf{Meas} \to \mathbf{QBS}\) sends a measurable space \(M\) to the QBS with \(M_{R(M)} = \{ f : \mathbb {R} \to M \mid f \text{ measurable}\} \).
If \(P : \mathbb {R} \to \mathbb {N}\) and each \(F_i : \mathbb {R} \to M\) are measurable, then \(\lambda r.\; F_{P(r)}(r)\) is measurable. This justifies the gluing axiom for \(R(M)\).
\(\mathtt{realQ} = R(m\mathbb {R})\), \(\mathtt{natQ} = R(\mathbb {N})\), \(\mathtt{boolQ} = R(\mathbb {B})\).
If \(f : M_1 \to M_2\) is measurable, then \(f\) is a QBS morphism \(R(M_1) \to R(M_2)\).
\(\mathrm{id}\) is a QBS morphism \(R(M) \to R(M)\).
If \(f, g\) are measurable, then \(g \circ f\) is a QBS morphism \(R(M_1) \to R(M_3)\).
1.4 Binary Products
The product \(X \times Y\) of two QBS has random elements \(M_{X \times Y} = \{ \alpha \mid \pi _1 \circ \alpha \in M_X \text{ and } \pi _2 \circ \alpha \in M_Y\} \).
\(\mathrm{fst} : X \times Y \to X\) is a QBS morphism.
\(\mathrm{snd} : X \times Y \to Y\) is a QBS morphism.
If \(f : W \to X\) and \(g : W \to Y\) are QBS morphisms, then \(\langle f, g \rangle : W \to X \times Y\) is a QBS morphism.
If \(\alpha \in M_Y\), then \(\lambda r.\; (x, \alpha (r)) \in M_{X \times Y}\).
If \(\alpha \in M_X\), then \(\lambda r.\; (\alpha (r), y) \in M_{X \times Y}\).
\((x, y) \mapsto (y, x)\) is a QBS morphism \(X \times Y \to Y \times X\).
\(((x,y),z) \mapsto (x,(y,z))\) is a QBS morphism.
\((x,(y,z)) \mapsto ((x,y),z)\) is a QBS morphism.
1.5 Exponentials (Function Spaces)
The exponential \(X \Rightarrow Y\) has carrier the set of QBS morphisms \(X \to Y\), with a function \(g : \mathbb {R} \to (X \to Y)\) random iff the uncurried map \((r, x) \mapsto g(r)(x)\) is a QBS morphism \(\mathbb {R} \times X \to Y\).
Evaluation \((f, x) \mapsto f(x)\) is a QBS morphism \((X \Rightarrow Y) \times X \to Y\).
If \(f : X \times Y \to Z\) is a QBS morphism, then \(\hat{f} : X \to (Y \Rightarrow Z)\) defined by \(\hat{f}(x)(y) = f(x,y)\) is a QBS morphism.
The category of quasi-Borel spaces is cartesian closed.
Given QBS morphisms \(f : W \to (X \Rightarrow Y)\) and \(g : W \to X\), the pointwise application \(w \mapsto f(w)(g(w))\) is a QBS morphism \(W \to Y\).
1.6 Unit QBS
The unit QBS has carrier \(\mathtt{unit}\) with every function random: \(M_{\mathtt{unit}} = \{ f : \mathbb {R} \to \mathtt{unit}\} \).
The unique map \(X \to \mathtt{unit}\) is a QBS morphism (terminality).
1.7 Induced Sigma-Algebra
For a QBS \(X\), the induced sigma-algebra is \(\sigma _{M_X} = \{ U \subseteq X \mid \forall \alpha \in M_X,\; \alpha ^{-1}(U) \text{ is Borel measurable}\} \).
\(\sigma _{M_X}\) is a sigma-algebra: it contains the full set, is closed under complement, and is closed under countable union.
1.8 Arithmetic Morphisms
\((x, y) \mapsto x + y\) is a QBS morphism \(\mathtt{realQ} \times \mathtt{realQ} \to \mathtt{realQ}\).
\((x, y) \mapsto x \cdot y\) is a QBS morphism \(\mathtt{realQ} \times \mathtt{realQ} \to \mathtt{realQ}\).
\((x, y) \mapsto (x {\lt} y)\) is a QBS morphism \(\mathtt{realQ} \times \mathtt{realQ} \to \mathtt{boolQ}\).
\(\mathtt{negb}\) is a QBS morphism \(\mathtt{boolQ} \to \mathtt{boolQ}\).
1.9 Subspaces
Given a QBS \(X\) and a predicate \(P \subseteq X\), the subspace QBS has carrier \(\{ x : X \mid P(x)\} \) with \(\alpha \) random iff \(\mathrm{proj}_1 \circ \alpha \in M_X\).
1.10 Generating QBS
Given a set \(G\) of functions \(\mathbb {R} \to T\), the generating QBS is the smallest QBS containing \(G\), constructed by inductive closure under composition, constants, and gluing.
\(G \subseteq M_{\mathrm{gen}(G)}\).
If \(M'\) satisfies the QBS axioms and \(G \subseteq M'\), then \(M_{\mathrm{gen}(G)} \subseteq M'\).
1.11 Image QBS
Given a QBS morphism \(f : X \to Y\), the image QBS \(\mathrm{im}(f)\) is \(\mathrm{gen}(\{ f \circ \alpha \mid \alpha \in M_X\} )\).
If \(\alpha \in M_X\), then \(f \circ \alpha \in M_{\mathrm{im}(f)}\).
\(M_{\mathrm{im}(f)} \subseteq M_Y\).
If \(g : Y \to Z\) is a QBS morphism, then \(g\) is also a morphism from the image QBS.
\(f\) is a QBS morphism \(X \to \mathrm{im}(f)\).
1.12 Order Structure on QBS
For QBS structures on the same carrier \(T\), \(M_X \leq M_Y\) iff \(M_X \subseteq M_Y\) (more random elements means coarser structure).
\(\leq \) is reflexive, transitive, and antisymmetric.
The supremum of two QBS structures on \(T\) is \(\mathrm{gen}(M_X \cup M_Y)\).
The supremum is an upper bound for both components and is the least such upper bound.
1.13 The L Functor and L–R Adjunction
The functor \(L : \mathbf{QBS} \to \sigma \text{-}\mathbf{Alg}\) sends a QBS \(X\) to its induced sigma-algebra \(\sigma _{M_X}\).
\(L(X)\) satisfies \(\emptyset , T \in L(X)\), closure under complement, and closure under countable union.
If \(f : X \to Y\) is a QBS morphism and \(U \in L(Y)\), then \(f^{-1}(U) \in L(X)\).
\(L\) preserves identity and composition.
A function \(f : X \to M\) is a QBS morphism \(X \to R(M)\) if and only if it pulls back measurable sets to \(L(X)\)-measurable sets:
This is a single-object biconditional, not a full categorical naturality statement (the functorial squares are not formalized).
The left-to-right direction (lr_adj_l2r) composes \(\alpha ^{-1}\) with the QBS morphism condition. The right-to-left direction (lr_adj_r2l) uses the measurability hypothesis to verify \(f \circ \alpha \) is measurable for each random element.
\(R(M_1 \times M_2)\) and \(R(M_1) \times R(M_2)\) have the same random elements.
If \(\alpha \in M_X\) and \(U \in \sigma _{M_X}\), then \(\alpha ^{-1}(U)\) is Borel measurable.
If \(U\) is measurable in \(M\), then \(U \in L(R(M))\).
1.14 Standard Borel Spaces (Definition)
A measurable space \(M\) is standard Borel if there exist measurable \(f : M \to \mathbb {R}\) and \(g : \mathbb {R} \to M\) with \(g \circ f = \mathrm{id}\).
\(\mathbb {R}\) is standard Borel via the identity functions.
If \(M_1\) and \(M_2\) are standard Borel and \(f : M_1 \to M_2\) is a QBS morphism \(R(M_1) \to R(M_2)\), then \(f\) is measurable.
Factor \(f = \psi _2 \circ (\phi _2 \circ f \circ \psi _1) \circ \phi _1\) through the standard Borel witnesses and use the QBS morphism condition on the measurable \(\psi _1\) to obtain measurability.
\(\mathbb {N}\) is standard Borel.
\(\mathrm{bool}\) is standard Borel.
If \(M_1\) and \(M_2\) are standard Borel, then \(M_1 \times M_2\) is standard Borel.
The extended reals \(\bar{\mathbb {R}}\) form a standard Borel space.
For a standard Borel space \(M\), the \(L(R(M))\)-measurable sets coincide with the original measurable sets.
1.15 Coproducts (Binary)
The coproduct \(X + Y\) has random elements that factor through \(\mathrm{inl}\), through \(\mathrm{inr}\), or through a measurable boolean predicate switching between the two.
\(\mathrm{inl} : X \to X + Y\) and \(\mathrm{inr} : Y \to X + Y\) are QBS morphisms.
If \(f : X \to Z\) and \(g : Y \to Z\) are QBS morphisms, then the case-analysis function \([f, g] : X + Y \to Z\) is a QBS morphism.
1.16 Coproducts (General / Sigma Type)
For a measurable index type \(I\) and a family \(X : I \to \mathbf{QBS}\), the general coproduct \(\coprod _{i:I} X_i\) has carrier \(\{ i : I ~ \& ~ X_i\} \) (dependent sum). A random element \(\alpha \) factors as \(\alpha (r) = (P(r), F_{P(r)}(r))\) for measurable \(P : \mathbb {R} \to I\) and family \(F_i \in M_{X_i}\).
For each \(i : I\), the injection \(x \mapsto (i, x)\) is a QBS morphism \(X_i \to \coprod _j X_j\).
The binary coproduct \(X + Y\) embeds into (and out of) the general coproduct over \(\mathbb {B}\).
1.17 Dependent Products (Pi Type)
For a family \(X : I \to \mathbf{QBS}\), the dependent product \(\prod _{i:I} X_i\) has \(\alpha \) random iff for every \(i : I\), \(\lambda r.\; \alpha (r)(i) \in M_{X_i}\).
For each \(i : I\), the projection \(f \mapsto f(i)\) is a QBS morphism \(\prod _j X_j \to X_i\).
If \(f_i : W \to X_i\) are QBS morphisms for all \(i\), then \(w \mapsto (\lambda i.\; f_i(w))\) is a QBS morphism \(W \to \prod _i X_i\).
1.18 List Type
For a QBS \(X\) with inhabitant \(x_0 : X\), the list QBS \(\mathrm{list}(X)\) has \(\alpha \) random iff there exist measurable \(\mathrm{len} : \mathbb {R} \to \mathbb {N}\) and random \(F_i \in M_X\) such that \(\alpha (r) = \mathrm{mkseq}(\lambda i.\; F_i(r), \mathrm{len}(r))\).
\(\mathrm{size} : \mathrm{list}(X) \to \mathtt{natQ}\) is a QBS morphism.
If \(\alpha \in M_{\mathrm{list}(X)}\), then \(\lambda r.\; \mathrm{nth}\; x_0\; (\alpha (r))\; i \in M_X\).