Quasi-Borel Spaces

The notion of quasi-Borel spaces was introduced by Heunen et al. The theory provides a suitable denotational model for higher-order probabilistic programming languages with continuous distributions. This entry is a formalization of the theory of quasi-Borel spaces, including construction of quasi-Borel spaces (product, coproduct, function spaces), the adjunction between the category of measurable spaces and the category of quasi-Borel spaces, and the probability monad on quasi-Borel spaces. This entry also contains the formalization of the Bayesian regression presented in the work of Heunen et al. This work is a part of the work by same authors, Program Logic for Higher-Order Probabilistic Programs in Isabelle/HOL, which will be published in the proceedings of the 16th International Symposium on Functional and Logic Programming (FLOPS 2022).