the apple monad

Stream: general

[Johan Commelin]

Welcome back @Johannes Hölzl :wave: :apple: :octopus:

[Johannes Hölzl]

This is not work related.

[Johannes Hölzl]

It is nice to see that I finally see an application of category theory. I think proving Ionescu Tulcea, i.e. that the Giry monad (on probability measures) allows us to construct Markov processes, can be simplified using some general constructions.

[Johan Commelin]

This is not work related.

Sure, but it's nevertheless very nice to see this activity (-;

[Johan Commelin]

And yes, an application of category theory is really nice.

[Koundinya Vajjha]

It is nice to see that I finally see an application of category theory. I think proving Ionescu Tulcea, i.e. that the Giry monad (on probability measures) allows us to construct Markov processes, can be simplified using some general constructions.

I would like to thank you @Johannes Hölzl for your measure theory library. It has been really spectacular. (I almost wept with delight when I discovered the induction_on_inter version of Dynkin's theorem.)