Contents

# Contents

### Ideas

$P(A|B) \cdot P(B) = P(B|A) \cdot P(A)$ resembles the way of breaking up a type as a dependent sum.

Take non-dependent types. Then $\sum_{x:A}B \simeq \sum_{y:B}A$. So There is an equivalence between distributions on these which will map between $z_1: D(A), z_2: [A, D(B)]$ and $w_1: D(B), w_2: [B, D(A)]$.

$w_1(b) = \sum_{a:A}z_1(a).z_2(a)(b); w_2(b)(a) =z_2(a)(b).z_1(a)/w_1(b).$

What happens when there is true dependence? Such as anaphora,

Prob(Jill comes tumbling after him|Jack falls down).

(Sam Staton points to disintegration

$D(\sum_{a : A} (B a)) \to \prod_{a : A} (D(B a))$

Seems like the dependent linear De Morgan duality (Prop. 3.18, p. 43) of Urs’s paper

(Note his pointer to here.)

Perhaps that’s not surprising if we take $D(X)$ as some subobject of $[X, \mathbb{R}^{\geq 0}]$.

People are certainly thinking of $[0,1]$ playing a dualizing role

The role played by the two-element set $\{0,1\}$ in these classical results—e.g.as “schizophrenic” object—is played in our probabilistic analogues by the unit interval $[0,1]$ (The Expectation Monad in Quantum Foundations, p. 2)

Take a simple case of tossing a coin until the first Head. If iterated dependent sum needs terms of the same length, we could construe things as though after reaching H, it returns H with probability 1.

Markov processes and dependency.

### References

Probability theory meets type theory and/or category theory:

• Topos Institute workshop

• Bart Jacobs, Fabio Zanasi, and Octavio Zapata, Bayesian Factorisation as Adjoint, abstract Adjunction between Bayesian nets and distributions. How can one net be assigned?

• Bart Jacobs, Structured Probabilistic Reasoning, pdf

• Bart Jacobs, Categorical Aspects of Parameter Learning, slides

• Kenta Cho, Bart Jacobs, Disintegration and Bayesian Inversion via String Diagrams, (arXiv:1709.00322)

• Bart Jacobs, Sam Staton, De Finetti’s construction as a categorical limit, (arXiv:2003.01964)

• Jonathan H. Warrell, A Probabilistic Dependent Type System based on Non-Deterministic Beta Reduction, (arXiv:1602.06420)

• Jonathan Warrell, Mark Gerstein, Dependent Type Networks: A Probabilistic Logic via the Curry-Howard Correspondence in a System of Probabilistic Dependent Types (pdf)

• Gianluca Giorgolo, Ash Asudeh, One Semiring to Rule Them All, (pdf)

• Harry Crane, Logic of probability and conjecture, (pdf) (longer version in progress)

• Bob Coecke, Eric Oliver Paquette, Dusko Pavlovic, Classical and quantum structuralism, (arXiv:0904.1997)

• Bob Coecke, Robert W. Spekkens, Picturing classical and quantum Bayesian inference, (arXiv:1102.2368)

• Robin Adams, Bart Jacobs, A Type Theory for Probabilistic and Bayesian Reasoning, (arXiv:1511.09230)

• Bart Jacobs, Fabio Zanasi, The Logical Essentials of Bayesian Reasoning, (arXiv:1804.01193)

• Bart Jacobs, Aleks Kissinger, Fabio Zanasi, Causal Inference by String Diagram Surgery, (arXiv:1811.08338)

• Julian Hough, Matthew Purver, Probabilistic Type Theory for Incremental Dialogue Processing, (pdf)

• Krasimir Angelov, Probability Distributions in Type Theory with Applications in Natural Language Syntax

• Tobias Fritz, Paolo Perrone, Bimonoidal Structure of Probability Monads, (arXiv:1804.03527)

• Tobias Fritz, Paolo Perrone, A Probability Monad as the Colimit of Finite Powers, (arXiv:1712.05363)

• Paolo Perrone, Categorical Probability and Stochastic Dominance in Metric Spaces, (thesis)

• Tobias Fritz? and Paolo Perrone, A Probability Monad as the Colimit of Spaces of Finite Samples, (arXiv:1712.05363).

• Tobias Fritz, A synthetic approach to Markov kernels, conditional independence, and theorems on sufficient statistics, (arXiv:1908.07021)

• Tobias Fritz, Paolo Perrone, Sharwin Rezagholi, Probability, valuations, hyperspace: Three monads on Top and the support as a morphism, (arXiv:1910.03752)

• Alex Simpson, Synthetic probability theory, slides

• Alex Simpson, Probability Sheaves and the Giry Monad, (pdf)

• B. Jacobs. New directions in categorical logic, for classical, probabilistic and quantum logic. Logical Methods in Computer Science, 11(3):1–76, 2015

• Kirk Sturtz, Categorical Probability Theory (arXiv:1406.6030) + others

• Norman Ramsey, Avi Pfeffer, Stochastic Lambda Calculus and Monads of Probability Distributions, (pdf).

• Chris Heunen, Ohad Kammar, Sam Staton, Hongseok Yang, A Convenient Category for Higher-Order Probability Theory, (arXiv:1701.02547)

• Matthijs Vákár, Ohad Kammar, Sam Staton, A Domain Theory for Statistical Probabilistic Programming, (arXiv:1811.04196)

• Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, Zoubin Ghahramani, Denotational validation of higher-order Bayesian inference, (arXiv:1711.03219)

• A. Ścibior, Z. Ghahramani, and A. D. Gordon, Practical probabilistic programming with monads, In Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, pages 165–176. ACM, 2015. (pdf)

• A. Ścibior, A.D.Gordon, Parameterized probability monad, (pdf)

• Flori C. (2013) Probabilities in Topos Quantum Theory. In: A First Course in Topos Quantum Theory. Lecture Notes in Physics, vol 868. Springer, Berlin, Heidelberg

• Juan Pablo Vigneaux, Generalized information structures and their cohomology, (arXiv:1709.07807)

• Florian Faissole and Bas Spitters, Synthetic topology in Homotopy Type Theory for probabilistic programming, (pdf)

• Ugo Dal Lago, Naohiko Hoshino, The Geometry of Bayesian Programming, (arXiv:1904.07425)

• Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Aleš Bizjak, Marco Gaboardi, Deepak Garg, Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus, (arXiv:1802.09787)

• Pieter Collins, Computable Stochastic Processes, (arXiv:1409.4667)

• Prakash Panangaden, A categorical view of conditional expectation, (slides)

• Dario Stein, Sam Staton, Compositional Semantics for Probabilistic Programs with Exact Conditioning, (arXiv:2101.11351)

• Bart Jacobs, A Channel-Based Perspective on Conjugate Priors, (arXiv:1707.00269)

• Dan Shiebler, Categorical Stochastic Processes and Likelihood,(arXiv:2005.04735)

For big picture in probability theory see answers to

• John C. Baez, Jacob D. Biamonte, A course on quantum techniques for stochastic mechanics, pdf

Discussion from a perspective of formal logic/type theory is in

• Neil Toronto, Useful Languages for Probabilistic Modeling and Inference, PhD Thesis, 2014 (pdf, slides)

Homotopy probability theory