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.

翻译：微分线性逻辑（DiLL）是一种通过线性公式与非线性公式之间的对称性来表达微分的相继式演算。本文中将DiLL的范畴模型表示为一对配备切函子的格罗滕迪克纤维化。为此，我们将类型论范畴语义的方法适配到线性-非线性伴随结构。这是迈向统一DiLL与依赖类型的第一步。