### Domain types based on probability monads

(Important: I did not create the image shown in blogger preview - it is from NCat Lab website!) 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 world Compile-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 proce