2025/07/16 by Daniel Rogozin, Rogozin, Daniel
#math.LO #math.CT
paper · pdf · doi:10.48550/arxiv.2507.12360
In this paper, we present a typed lambda calculus \bf SILL(λ)Σ, a type-theoretic version of intuitionistic multiplicative linear logic with subexponentials, that is, we have many comonadic resource modalities with some interconnections between them given by a subexponential signature Σ. We introduce the concept of a Σ-assemblage to characterise models of \bf SILL(λ)Σ to expand the concept of a linear category where one has multiple resource comonads and symmetric lax monoidal comonad morphisms. We also generalise several known results from linear logic and show that every Σ-assemblage can be viewed as a symmetric monoidal closed category equipped with a family of monoidal adjunctions and morphisms by modernising and generalising Benton's results by involving the formal theory of comonads in the fashion of Street. We give a stronger 2-categorical characterisation of Σ-assemblages and show that the 2-category of Σ-assemblages 1,2-fully faithfully embeds into the category of Σ-boutons, that is, polymodal expansions of linear-non-linear models. In the final section, we describe realisability models for the particular case of \bf SILL(λ)Σ3 for a three-element subexponential signature Σ3 by describing BCI algebras with extra operators viewed as applicative morphisms and assemblies and modest sets over them.