Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: event: Categorical Probability and Statistics 2020 workshop

Topic: Jun 7: Bas Spitters' talk

Paolo Perrone (Jun 04 2020 at 19:15):

Hey all,
This is the discussion thread of Bas Spitters' talk, "Synthetic topology in Homotopy Type Theory for probabilistic programming".
The talk, besides being on Zoom, is livestreamed here: https://youtu.be/NI0L9tWQg04

Paolo Perrone (Jun 04 2020 at 19:23):

Date and time: Sunday, 7 Jun, 13h UTC.

Paolo Perrone (Jun 07 2020 at 12:50):

Hello! We start in 10 minutes.

Robert Furber (Jun 07 2020 at 13:05):

Something is wrong with the Youtube livestream - it keeps cutting in and out.

Robert Furber (Jun 07 2020 at 13:05):

I've just got a spinning circle thing with a still image.

Peter Arndt (Jun 07 2020 at 13:06):

Same here

Paolo Perrone (Jun 07 2020 at 13:08):

Looking into that, sorry. It seems to be a problem upstream (with Zoom). The Zoom call is fine though, you may want to connect to Zoom while I try to fix the problem.

Paolo Perrone (Jun 07 2020 at 13:09):

Should be better now

Robert Furber (Jun 07 2020 at 13:10):

It's improved.

Unfortunately I'm told that when I use Zoom my microphone produces a continuous high-pitched noise, and it is unreliable for me in other areas as well.

Paolo Perrone (Jun 07 2020 at 13:11):

According to my Youtube monitor, this seems fixed. Do you all confirm?

Paolo Perrone (Jun 07 2020 at 13:11):

Robert Furber said:

It's improved.

Unfortunately I'm told that when I use Zoom my microphone produces a continuous high-pitched noise, and it is unreliable for me in other areas as well.

Yeah, I totally understand (that's why we want to provide the Youtube option as well). Sorry about that problem, should be fixed.

Robert Furber (Jun 07 2020 at 13:12):

It's fine for me now.

Peter Arndt (Jun 07 2020 at 13:13):

yes, it works

Paolo Perrone (Jun 07 2020 at 13:13):

Great!

Paolo Perrone (Jun 07 2020 at 13:21):

Some context maybe: https://ncatlab.org/nlab/show/correspondence+between+measure+and+valuation+theory

Robert Furber (Jun 07 2020 at 13:26):

Isn't it the case that the constructive Riesz rep theorem is for continuous valuations, not the merely omega-continuous?

Robert Furber (Jun 07 2020 at 13:28):

(I fully admit that we can rule out those compact Hausdorff spaces where the two do not coincide for computability purposes)

Paolo Perrone (Jun 07 2020 at 13:35):

Robert Furber said:

Isn't it the case that the constructive Riesz rep theorem is for continuous valuations, not the merely omega-continuous?

By the way, I've forwarded this question to the chair - Prakash said it will be asked at the end.

Robert Furber (Jun 07 2020 at 13:46):

:clap:

Sam Staton (Jun 07 2020 at 13:49):

Hi Bas. Thanks for your talk. Yesterday Manuel Bärenz was asking about encoding symmetries and exchangeability using HOTT. Wonder if you've thought about that.

Manuel Bärenz (Jun 07 2020 at 13:53):

Yes, that would be super interesting! But I'm getting the impression that HoTT is "only" (mainly?) used for the implementation and reasoning about the topos, but it's not possible to have probabilities on, say, a a higher inductive type, only on internal sets?

Bas Spitters (Jun 07 2020 at 14:05):

@Sam Staton @Manuel Bärenz that's a good question. Yes, currently we are not using the higher structure.
Although, structure invariance holds in this model, for example.
I imagine that the quasitopos that Sam is studying could also be extended to a higher topos, so that could be another way of using HoTT.

Manuel Bärenz (Jun 07 2020 at 14:08):

Ah ok, so my question is actually related to @Tobias Fritz ' question, he asked whether any higher structure can be used, right?

Tobias Fritz (Jun 07 2020 at 14:18):

Yes, we seem to have been thinking along similar lines. Only semi-seriously: In the interest of HoTT taking over the world, it would help if one could argue that the codomain of a measure/valuation really wants to be a type with nontrivial higher homotopical structure instead of just the reals. In the sense that perhaps using real-valued probabilities is a mere "degroupoidification" of what probabilities actually ought to be. Just a wacky idea :P

Sam Staton (Jun 07 2020 at 14:44):

I think I answered @Dario Stein too quickly (I'm in a noisy house).
I think Bas is saying that a valuation on $X$ is a function that assigns to every $X\to\mathbb{S}$ a probability. (Correct me if I'm wrong.)

If you use measures instead of valuations in a topos, you would be tempted to look at functions that assign to every $X\to 2$ a probability. To borrow from Bas/Brouwer/etc, "all sets are measurable". But if you do this, you need to be careful with Fubini, as I mentioned in my talk. In quasi-Borel spaces we focused on those measures that arise as pushforwards from a fixed base measure, and then Fubini is easy. So there's a difference there from the topological approach.

Bas Spitters (Jun 07 2020 at 16:01):

Yes, that seems correct.
About your question about Randon-Nykodym. There is a constructive proof by Bishop. Since our work is quite close to Bishop's work, but localic, I believe we could do something similar. Let me know if you want more details.

Bas Spitters (Jun 07 2020 at 16:36):

There was a question after my talk whether we'd have a Markov category. I did not get who asked it.
The third example (Kleisli category) construction here should more or less work.
https://ncatlab.org/nlab/show/Markov+category
However, our Giry monad need not be commutive on the full topos, however Fubini holds on Locales, as shown by Vickers.
So, the Giry monad on locales should form a Markov category. @Tobias Fritz @Eigil Rischel Does this make sense?

Dario Stein (Jun 07 2020 at 17:14):

Sam Staton said:

I think I answered Dario Stein too quickly (I'm in a noisy house).
I think Bas is saying that a valuation on $X$ is a function that assigns to every $X\to\mathbb{S}$ a probability. (Correct me if I'm wrong.)

If you use measures instead of valuations in a topos, you would be tempted to look at functions that assign to every $X\to 2$ a probability. To borrow from Bas/Brouwer/etc, "all sets are measurable". But if you do this, you need to be careful with Fubini, as I mentioned in my talk. In quasi-Borel spaces we focused on those measures that arise as pushforwards from a fixed base measure, and then Fubini is easy. So there's a difference there from the topological approach.

Thanks Sam. I was surprised by the connection as I hadn't thought much about how probability might look internally in quasi-Borel spaces. I thought there was maybe something intrinsically nicer about topology as opposed to measurability that makes it preferable as a foundation to build a topos upon. For example, covers in topology encode a lot of information (leading to the concept of compactness) whereas there seems no nice measurable analogue. Compactness also makes topological function spaces sort-of possible (see CHaus), whereas in Meas cartesian closure fails utterly.

Bas Spitters (Jun 07 2020 at 17:19):

@Sam Staton @Dario Stein Has the internal logic of the quasitopos of quasi-borel spaces been worked out?

John Baez (Jun 07 2020 at 18:20):

Tobias Fritz said:

Only semi-seriously: In the interest of HoTT taking over the world, it would help if one could argue that the codomain of a measure/valuation really wants to be a type with nontrivial higher homotopical structure instead of just the reals. In the sense that perhaps using real-valued probabilities is a mere "degroupoidification" of what probabilities actually ought to be. Just a wacky idea :P

I've been thinking that this wacky idea could be exciting as part of a categorification of the basic ideas of quantum physics: make amplitudes and probabilities be elements in a chain complex or some other sort of higher structure.'

People are already using $L_\infty$-algebras instead of Lie algebras to describe symmetries in quantum physics, and probably $A_\infty$-algebras to describe "algebras of observables".

Sam Staton (Jun 07 2020 at 20:45):

Bas Spitters said:

However, our Giry monad need not be commutive on the full topos

Ah, that's very interesting. (I thought you might have got away with it for some reason.) Instead of cutting down to locales, might you instead get a commutative monad by cutting down to certain valuations? as we did with quasi-Borel spaces?

Paolo Perrone (Jun 07 2020 at 22:05):

Hey all! Here's the video.
https://youtu.be/HWJNYO7EnoQ

Alexander Shamov (Jun 08 2020 at 01:36):

John Baez said:

Tobias Fritz said:

Only semi-seriously: In the interest of HoTT taking over the world, it would help if one could argue that the codomain of a measure/valuation really wants to be a type with nontrivial higher homotopical structure instead of just the reals. In the sense that perhaps using real-valued probabilities is a mere "degroupoidification" of what probabilities actually ought to be. Just a wacky idea :P

I've been thinking that this wacky idea could be exciting as part of a categorification of the basic ideas of quantum physics: make amplitudes and probabilities be elements in a chain complex or some other sort of higher structure.'

People are already using $L_\infty$-algebras instead of Lie algebras to describe symmetries in quantum physics, and probably $A_\infty$-algebras to describe "algebras of observables".

There's a much simpler idea: this higher homotopical measure theory could be a homology theory dual to "continuous cohomology". Meaning, we can just integrate functions with values in an Eilenberg-Maclane spectrum of R, rather than in R itself.
Even classically, and without any topology: if we take the category of "standard Lebesgue spaces" (aka mesurable locales aka commutative W*-algebras) and form a sheaf topos out of it, this topos will contain "bad" objects like ergodic quotients. By resolving them into simplicial representable objects and applying the functor of signed finite variation measures, we get simplicial vector spaces, hence higher "measure homologies". My guess would be that they can be nontrivial. I don't know if this is something people already do in ergodic theory...

Bas Spitters (Jun 08 2020 at 15:31):

@Sam Staton In section 7 here I've developed a constructive and algebraic version of Radon-Nikodym. It an algebraic formulation of the work by Bishop and Bridges. The key insight (by them) is that one can use the Riesz representation theorem for the Hilbert space L2. However, this requires some continuity conditions on the functional which we need to carry over to the definition of absolute continuity.
I'm curious whether L2 shows up anywhere in the work on Radon-Nikodym by @Prakash Panangaden

Robert Furber (Jun 08 2020 at 15:37):

Bas, is that proof related to von Neumann's proof: https://planetmath.org/proofofradonnikodymtheorem

Robert Furber (Jun 08 2020 at 15:38):

Von Neumann used the L2 Riesz rep. thm. to prove the sigma-finite Radon-Nikodym theorem.

Bas Spitters (Jun 08 2020 at 15:48):

@Robert Furber Yes! Thanks for the addition.