License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CALCO.2021.19
URN: urn:nbn:de:0030-drops-153742
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/15374/
Lemay, Jean-Simon Pacaud
Coderelictions for Free Exponential Modalities
Abstract
In a categorical model of the multiplicative and exponential fragments of intuitionistic linear logic (MELL), the exponential modality is interpreted as a comonad ! such that each cofree !-coalgebra !A comes equipped with a natural cocommutative comonoid structure. An important case is when ! is a free exponential modality so that !A is the cofree cocommutative comonoid over A. A categorical model of MELL with a free exponential modality is called a Lafont category. A categorical model of differential linear logic is called a differential category, where the differential structure can equivalently be described by a deriving transformation !A⊗A →{?_A} !A or a codereliction A →{η_A} !A. Blute, Lucyshyn-Wright, and O'Neill showed that every Lafont category with finite biproducts is a differential category. However, from a differential linear logic perspective, Blute, Lucyshyn-Wright, and O'Neill’s approach is not the usual one since the result was stated in the dual setting and the proof is in terms of the deriving transformation ?. In differential linear logic, it is often the codereliction η that is preferred and that plays a more prominent role. In this paper, we provide an alternative proof that every Lafont category (with finite biproducts) is a differential category, where we construct the codereliction η using the couniversal property of the cofree cocommtuative comonoid !A and show that η is unique. To achieve this, we introduce the notion of an infinitesimal augmentation k⊕A →{?_A} !(k ⊕ A), which in particular is a !-coalgebra and a comonoid morphism, and show that infinitesimal augmentations are in bijective correspondence to coderelictions (and deriving transformations). As such, infinitesimal augmentations provide a new equivalent axiomatization for differential categories in terms of more commonly known concepts. For a free exponential modality, its infinitesimal augmentation is easy to construct and allows one to clearly see the differential structure of a Lafont category, regardless of the construction of !A.
BibTeX - Entry
@InProceedings{lemay:LIPIcs.CALCO.2021.19,
author = {Lemay, Jean-Simon Pacaud},
title = {{Coderelictions for Free Exponential Modalities}},
booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
pages = {19:1--19:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-212-9},
ISSN = {1868-8969},
year = {2021},
volume = {211},
editor = {Gadducci, Fabio and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/15374},
URN = {urn:nbn:de:0030-drops-153742},
doi = {10.4230/LIPIcs.CALCO.2021.19},
annote = {Keywords: Differential Categories, Coderelictions, Differential Linear Logic, Free Exponential Modalities, Lafont Categories, Infinitesimal Augmentations}
}
|
Keywords: |
|
Differential Categories, Coderelictions, Differential Linear Logic, Free Exponential Modalities, Lafont Categories, Infinitesimal Augmentations |
|
Collection: |
|
9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021) |
|
Issue Date: |
|
2021 |
|
Date of publication: |
|
08.11.2021 |
