Double glueing over free exponential: With measure theoretic applications

This paper provides a compact method to lift the free exponential construction of Melliès-Tabareau-Tasson over the Hyland-Schalk double glueing for orthogonality categories. A condition ”reciprocity of orthogonality” is shown simply enough to lift the free exponential over the double glueing in terms of the orthogonality. Our general method applies to the monoidal category TsK of the s-finite transition kernels with countable biproducts. We show (i) TsK op has the free exponential, which is shown to be describable in terms of measure theory. (ii) The s-finite transition kernels have an orthogonality between measures and measurable functions in terms of Lebesgue integrals. The orthogonality has the reciprocity, hence the free exponential of (i) lifts to the orthogonality category O I ( TsK op ) , which subsumes Ehrhard et al’s probabilistic coherent spaces as a full subcategory of countable measurable spaces. To lift the free exponential, the measure-theoretic uniform convergence theorem commuting Lebesgue integral and limit plays a crucial role as well as Fubini-Tonelli theorem for double integral in s-finiteness. Our measure-theoretic orthogonality is considered as a continuous version of the orthogonality of the probabilistic coherent spaces for linear logic, and in particular provides a two layered decomposition of Crubillé et al’s direct free exponential for these spaces arisen as discretisation in this paper.