There Is Only One Notion of Differentiation
J.R.B. Cockett, Jean-Simon Pacaud Lemay · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2017
Differential linear logic was introduced as a syntactic proof-theoretic approach to the analysis of differential calculus. Differential categories were subsequently introduce to provide a categorical model theory for differential linear logic. Differential categories used two different approaches for defining differentiation abstractly: a deriving transformation and a coderiliction. While it was thought that these notions could give rise to distinct notions of differentiation, we show here that these notions, in the presence of a monoidal coalgebra modality, are completely equivalent.