Coderelictions for Free Exponential Modalities
| Autor: | Lemay, Jean-Simon Pacaud |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: | |
| DOI: | 10.4230/lipics.calco.2021.19 |
| Popis: | 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. LIPIcs, Vol. 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021), pages 19:1-19:21 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|