Document Open Access Logo

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

Author Jean-Simon Pacaud Lemay

PDF
Thumbnail PDF

File

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

Document Identifiers

Author Details

Jean-Simon Pacaud Lemay
  • University of Oxford, Computer Science Department, Oxford, UK, https://www.cs.ox.ac.uk/people/jean-simon.lemay/

Funding

  • Lemay, Jean-Simon Pacaud: Funded by Kellogg College, the Clarendon fund, and the Department of Computer Science of the University of Oxford

Cite As Get BibTex

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
  • Bimonads
  • Differential Categories

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Jon Beck. Distributive laws. In Seminar on triples and categorical homology theory, pages 119-140. Springer, 1969. Google Scholar
  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. Google Scholar
  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. Google Scholar
  4. Richard Blute and Philip Scott. Category theory for linear logicians. Linear logic in computer science, 316:3-65, 2004. Google Scholar
  5. Richard F Blute. Hopf algebras and linear logic. Mathematical Structures in Computer Science, 6(2):189-212, 1996. Google Scholar
  6. Richard F Blute, J Robin B Cockett, and Robert AG Seely. Differential categories. Mathematical structures in computer science, 16(6):1049-1083, 2006. Google Scholar
  7. Alain Bruguieres, Steve Lack, and Alexis Virelizier. Hopf monads on monoidal categories. Advances in Mathematics, 227(2):745-800, 2011. Google Scholar
  8. Alain Bruguieres and Alexis Virelizier. Hopf monads. Advances in Mathematics, 215(2):679-733, 2007. Google Scholar
  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. Google Scholar
  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. Google Scholar
  11. Jean-Yves Girard. Linear logic. Theoretical computer science, 50(1):1-101, 1987. Google Scholar
  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. Google Scholar
  13. Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. Theoretical computer science, 294(1-2):183-231, 2003. Google Scholar
  14. S. Mac Lane. Categories for the working mathematician. Springer-Verlag, New York, Berlin, Heidelberg, 1971, revised 2013. Google Scholar
  15. Shahn Majid. Foundations of quantum group theory. Cambridge university press, 2000. Google Scholar
  16. Paddy McCrudden. Opmonoidal monads. Theory Appl. Categ, 10(19):469-485, 2002. Google Scholar
  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. Google Scholar
  19. Paul-André Mellies. Categorical semantics of linear logic. Panoramas et syntheses, 27:15-215, 2009. Google Scholar
  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. Google Scholar
  21. Ieke Moerdijk. Monads on tensor categories. Journal of Pure and Applied Algebra, 168(2):189-208, 2002. Google Scholar
  22. Andrea Schalk. What is a categorical model of linear logic. Manuscript, available from http://www. cs. man. ac. uk/ schalk/work. html, 2004. Google Scholar
  23. Robert AG Seely. Linear logic,*-autonomous categories and cofree coalgebras. Ste. Anne de Bellevue, Quebec: CEGEP John Abbott College, 1987. Google Scholar
  24. Ross Street. The formal theory of monads. Journal of Pure and Applied Algebra, 2(2):149-168, 1972. Google Scholar
  25. Donovan H Van Osdol. Sheaves in regular categories. In Exact Categories and Categories of Sheaves, pages 223-239. Springer, 1971. Google Scholar
  26. Robert Wisbauer. Algebras versus coalgebras. Applied Categorical Structures, 16(1):255-295, 2008. Google Scholar
  27. Marek Zawadowski. The formal theory of monoidal monads. Journal of Pure and Applied Algebra, 216(8-9):1932-1942, 2012. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact