Introduction

Quasi-Borel spaces solve a fundamental problem: the category of measurable spaces is not cartesian closed, which prevents giving semantics to higher-order probabilistic programs. QBS replaces measurable sets with “random elements” (morphisms from \(\mathbb {R}\)), yielding a cartesian-closed category with a well-behaved probability monad.

This formalization follows:

• C. Heunen, O. Kammar, S. Staton, H. Yang. A Convenient Category for Higher-Order Probability Theory. LICS 2017. https://arxiv.org/abs/1701.02547

• M. Hirata, Y. Minamide, T. Sato. Quasi-Borel Spaces. Archive of Formal Proofs, 2022. https://www.isa-afp.org/entries/Quasi_Borel_Spaces.html