A Fibrational Perspective on Differential Linear Logic

TL;DR

This paper presents a fibrational categorical framework for Differential Linear Logic, connecting it with tangent functors and aiming to unify DILL with dependent types.

Contribution

It introduces a fibrational model of DiLL using Grothendieck fibrations and tangent functors, advancing the categorical understanding of differential linear logic.

Findings

Categorical models of DiLL are expressed as pairs of Grothendieck fibrations with tangent functors.

Methods from categorical semantics of type theory are adapted to linear-non-linear adjunctions.

This work lays groundwork for unifying DILL with dependent types.

Abstract

Differential Linear Logic (DiLL) is a sequent calculus that expresses differentiation via symmetries between linear and non-linear formulas. In this paper, we express categorical models of DiLL as a pair of Grothendieck fibrations equipped with a tangent functor. To do so, we adapt methods from categorical semantics of type theory to linear-non-linear adjunctions. This is a first step towards unifying DILL and dependent types.