R.F. Blute, J.R.B. Cockett, J-S.P. Lemay, R.A.G. Seely
Differential categories were introduced to provide a minimal categorical doctrine for differential linear logic. Here we revisit the formalism and, in particular, examine the two different approaches to defining differentiation which were introduced. The basic approach used a deriving transformation, while a more refined approach, in the presence of a bialgebra modality, used a codereliction. The latter approach is particularly relevant to linear logic settings, where the coalgebra modality is monoidal and the Seely isomorphisms give rise to a bialgebra modality. Here, we prove that these apparently distinct notions of differentiation, in the presence of a monoidal coalgebra modality, are completely equivalent. Thus, for linear settings, there is only one notion of differentiation.
The paper also presents a number of separating examples for coalgebra modalities - which are and are not monoidal - which do and do not support differential structure. Of particular interest is the observation that - counter intuitively - differential algebras never form differential categories although they do have a monoidal coalgebra modality. On the other hand, Rota-Baxter algebras - which are usually associated with integration - provide an example of a differential category which has a non-monoidal coalgebra modality.
This is an extended version of "There is only one notion of differentiation." Cockett, R., & Lemay, J-S., 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017).