5. Kernelized monoidal composition🔗

The translation of kernels to morphisms in the SFinKer category allows us to adapt the ⊗≫ monoidal composition for kernels. The MeasurableCoherence class witnesses measurable equivalences between types, enabling an instance of categorical MonoidalCoherence that makes the kernelized monoidal composition ⊗≫ₖ possible.

5.1. Measurable Coherence🔗

The MeasurableCoherence class witnesses the existence of measurable equivalences between two measurable spaces. It acts as a kernel-level counterpart to the categorical MonoidalCoherence class:

class MeasurableCoherence (X Y : Type*) [MeasurableSpace X] [MeasurableSpace Y] where
  /-- A measurable equivalence between `X` and `Y`. -/
  miso : X ≃ᵐ Y

This class enables an instance of MonoidalCoherence between SFinKer objects at a common universe level via the monoidalCoherence function, using measurable equivalences from the original types.

This allows us to bridge the gap between the notion of measurable equivalence and the categorical notion of monoidal coherence, enabling the use of categorical machinery for kernel compositions.

5.2. Monoidal Composition of Kernels🔗

The kernelized monoidal composition ⊗≫ₖ is defined by composing two kernels while automatically handling measurable equivalences through the categorical framework:

Transport to SFinKer: Both kernels are translated to morphisms in the SFinKer category using the hom function, which lifts carrier spaces to a common universe level.
Categorical composition: The categorical monoidal composition ⊗≫ is applied to the resulting morphisms in SFinKer, which automatically inserts the necessary associators and unitors.
Transport back to kernels: The result is translated back to a kernel using the fromHom function.