Fibrational Semantics for Coexisting Implications

Most categorical semantics for systems combining intuitionistic and linear reasoning are organised around a modality or adjunction. Benton’s LNL models and Barber–Plotkin’s DILL models, for example, are built from symmetric monoidal adjunctions between a cartesian closed category and a symmetric monoidal closed category, with the modality (!) mediating between the intuitionistic and linear fragments. By contrast, the system we study here, TILL (Two-Implication Linear Lambda calculus, previously called ILT), is a non-modal double-context calculus in which both intuitionistic implication ($A\to B$) and linear implication ($A⊸B$) are primitive, and the modality (!) is absent from the syntax. TILL is therefore not simply a presentation of DILL or LNL: it isolates the coexistence of intuitionistic and linear implication without any added modality structure.

We give a fibrational semantics for TILL by linearising the fibrational semantics of the simply typed ($\lambda$)-calculus. Concretely, we replace the cartesian fibres of a Jacobs-style comprehension category with symmetric monoidal closed fibres, while keeping the base category cartesian to model intuitionistic contexts. The resulting TILL-indexed categories provide a sound and complete semantics for TILL, and TILL is their internal language.

This fibrational perspective also explains how TILL sits in relation to the better-known modal systems. Modal structure can be recovered from TILL-indexed categories, yielding connections with the classical categorical semantics of DILL and LNL; in particular, DILL appears as a conservative extension of TILL. The core fibrational idea goes back to earlier joint work of the authors, but the full construction and proofs were never published. We present them here in full, thereby supplying a categorical semantics for TILL itself, rather than only for modal systems built around (!). In this sense, the paper identifies the non-modal semantic core of coexisting intuitionistic and linear implication, while preserving the modular structure that makes many ordinary ($\lambda$)-calculus techniques and implementations available on the intuitionistic side.