Integrating function with values in LCS

Stream: maths

[Tomas Skrivan]

I found myself in the need of integrating function that have values in a locally convex vector space. I'm doing some source code transformations on probabilistic programs and I need this identity

(fun y => ∫ x, f x y) = (∫ x, fun y => f x y)

In a way, I can see it as a definition of the integral on the left by the integral on the right which can be Bochner integral.

In above f : X → Y → Z and X is some measure space , Y arbitrary type and Z is normed space.

This should generalize to arbitrary number of binders

(fun y z w => ∫ x, f x y z w) = (∫ x, fun y z w => x y z w)

What would be the best abstraction for this?