### Domain types for interactions with probability monads

Composed stochastic proof for low-dimensional applications Following up on previous post on Composed Stochastic Proof, we now enumerate:What the typed world owes the authored worldCompile-time access to categorical knowledge about probability monads (overview page at NCat Lab site) over our dependent type system for measure theory (at MathLib/Lean site). To knit this knowledge into useful, portable applications, we proceed with four major tasks:

**Task 1)**Starting from a shared library conceptual math knowledge, we identify**applicable categories**that are useful in our application model. The NCatLab website is a great current resource on existing work. The page on monads of probability, measures, and valuations contains this summary table of the most useful, widely known functional probability concepts. These are the core ingredient math concepts needed for robust, general processing of probability models in functional computing environments.**Task 2)**Build upon our chosen categories som…