Document

# Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories

## File

LIPIcs.FSCD.2018.21.pdf
• Filesize: 0.49 MB
• 20 pages

## Cite As

Jean-Simon Pacaud Lemay. Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 21:1-21:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSCD.2018.21

## Abstract

A categorical model of the multiplicative and exponential fragments of intuitionistic linear logic (IMELL), known as a linear category, is a symmetric monoidal closed category with a monoidal coalgebra modality (also known as a linear exponential comonad). Inspired by R. Blute and P. Scott's work on categories of modules of Hopf algebras as models of linear logic, we study Eilenberg-Moore categories of monads as models of IMELL. We define an IMELL lifting monad on a linear category as a Hopf monad - in the Bruguieres, Lack, and Virelizier sense - with a mixed distributive law over the monoidal coalgebra modality. As our main result, we show that the linear category structure lifts to Eilenberg-Moore categories of IMELL lifting monads. We explain how monoids in the Eilenberg-Moore category of the monoidal coalgebra modality can induce IMELL lifting monads and provide sources for such monoids. Along the way, we also define mixed distributive laws of bimonads over coalgebra modalities and lifting differential category structure to Eilenberg-Moore categories of exponential lifting monads.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Categorical semantics
• Theory of computation → Linear logic
##### Keywords
• Mixed Distributive Laws
• Coalgebra Modalities
• Linear Categories
• Differential Categories

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. Jon Beck. Distributive laws. In Seminar on triples and categorical homology theory, pages 119-140. Springer, 1969.
2. Gavin M Bierman. What is a categorical model of intuitionistic linear logic? In International Conference on Typed Lambda Calculi and Applications, pages 78-93. Springer, 1995.
3. R Blute, J Robin B Cockett, and Robert AG Seely. Cartesian differential storage categories. Theory and Applications of Categories, 30(18):620-686, 2015.
4. Richard Blute and Philip Scott. Category theory for linear logicians. Linear logic in computer science, 316:3-65, 2004.
5. Richard F Blute. Hopf algebras and linear logic. Mathematical Structures in Computer Science, 6(2):189-212, 1996.
6. Richard F Blute, J Robin B Cockett, and Robert AG Seely. Differential categories. Mathematical structures in computer science, 16(6):1049-1083, 2006.
7. Alain Bruguieres, Steve Lack, and Alexis Virelizier. Hopf monads on monoidal categories. Advances in Mathematics, 227(2):745-800, 2011.
8. Alain Bruguieres and Alexis Virelizier. Hopf monads. Advances in Mathematics, 215(2):679-733, 2007.
9. J Robin B Cockett and Jean-Simon Lemay. There is only one notion of differentiation. In LIPIcs-Leibniz International Proceedings in Informatics, volume 84. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017.
10. M.P. Fiore. Differential structure in models of multiplicative biadditive intuitionistic linear logic. In International Conference on Typed Lambda Calculi and Applications, pages 163-177. Springer, 2007.
11. Jean-Yves Girard. Linear logic. Theoretical computer science, 50(1):1-101, 1987.
12. Jean-Yves Girard and Yves Lafont. Linear logic and lazy computation. In International Joint Conference on Theory and Practice of Software Development, pages 52-66. Springer, 1987.
13. Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. Theoretical computer science, 294(1-2):183-231, 2003.
14. S. Mac Lane. Categories for the working mathematician. Springer-Verlag, New York, Berlin, Heidelberg, 1971, revised 2013.
15. Shahn Majid. Foundations of quantum group theory. Cambridge university press, 2000.
16. Paddy McCrudden. Opmonoidal monads. Theory Appl. Categ, 10(19):469-485, 2002.
17. Paul-André Mellies. Categorical models of linear logic revisited. Archive ouverte HAL, 2003. URL: https://hal.archives-ouvertes.fr/hal-00154229.
18. Paul-André Mellies. Comparing hierarchies of types in models of linear logic. Information and Computation, 189(2):202-234, 2004.
19. Paul-André Mellies. Categorical semantics of linear logic. Panoramas et syntheses, 27:15-215, 2009.
20. Paul-André Melliès, Nicolas Tabareau, and Christine Tasson. An explicit formula for the free exponential modality of linear logic. Mathematical Structures in Computer Science, pages 1-34, 2017.
21. Ieke Moerdijk. Monads on tensor categories. Journal of Pure and Applied Algebra, 168(2):189-208, 2002.
22. Andrea Schalk. What is a categorical model of linear logic. Manuscript, available from http://www. cs. man. ac. uk/ schalk/work. html, 2004.
23. Robert AG Seely. Linear logic,*-autonomous categories and cofree coalgebras. Ste. Anne de Bellevue, Quebec: CEGEP John Abbott College, 1987.
24. Ross Street. The formal theory of monads. Journal of Pure and Applied Algebra, 2(2):149-168, 1972.
25. Donovan H Van Osdol. Sheaves in regular categories. In Exact Categories and Categories of Sheaves, pages 223-239. Springer, 1971.
26. Robert Wisbauer. Algebras versus coalgebras. Applied Categorical Structures, 16(1):255-295, 2008.
27. Marek Zawadowski. The formal theory of monoidal monads. Journal of Pure and Applied Algebra, 216(8-9):1932-1942, 2012.
X

Feedback for Dagstuhl Publishing

### Thanks for your feedback!

Feedback submitted

### Could not send message

Please try again later or send an E-mail