Synthetic topology in Homotopy Type Theory for probabilistic programming

TL;DR

This paper introduces synthetic topology within Homotopy Type Theory to model continuous probability distributions, enabling rigorous formalization of probabilistic computations involving continuous measures.

Contribution

It develops a synthetic topology framework for continuous distributions in type theory, including valuations and integrals, extending measure theory in proof assistants.

Findings

Defined valuations and lower integrals on sets

Proved versions of Riesz and Fubini theorems

Constructed Lebesgue valuation for continuous distributions

Abstract

The ALEA Coq library formalizes measure theory based on a variant of the Giry monad on the category of sets. This enables the interpretation of a probabilistic programming language with primitives for sampling from discrete distributions. However, continuous distributions have to be discretized because the corresponding measures cannot be defined on all subsets of their carriers. This paper proposes the use of synthetic topology to model continuous distributions for probabilistic computations in type theory. We study the initial $\sigma$-frame and the corresponding induced topology on arbitrary sets. Based on these intrinsic topologies we define valuations and lower integrals on sets, and prove versions of the Riesz and Fubini theorems. We then show how the Lebesgue valuation, and hence continuous distributions, can be constructed.