Monoidal Company for Accessible Functors

Authors Henning Basold, Damien Pous, Jurriaan Rot

Thumbnail PDF


  • Filesize: 0.58 MB
  • 16 pages

Document Identifiers

Author Details

Henning Basold
Damien Pous
Jurriaan Rot

Cite AsGet BibTex

Henning Basold, Damien Pous, and Jurriaan Rot. Monoidal Company for Accessible Functors. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Distributive laws between functors are a fundamental tool in the theory of coalgebras. In the context of coinduction in complete lattices, they correspond to the so-called compatible functions, which enable enhancements of the coinductive proof technique. Amongst these, the greatest compatible function, called the companion, has recently been shown to satisfy many good properties. Categorically, the companion of a functor corresponds to the final object in a category of distributive laws. We show that every accessible functor on a locally presentable category has a companion. Central to this and other constructions in the paper is the presentation of distributive laws as coalgebras for a certain functor. This functor itself has again, what we call, a second-order companion. We show how this companion interacts with the various monoidal structures on functor categories. In particular, both the first- and second-order companion give rise to monads. We use these results to obtain an abstract GSOS-like extension result for specifications involving the second-order companion.
  • coalgebras
  • distributive laws
  • accessible functors
  • monoidal categories


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


  1. J. Adamek, S. Milius, and L Moss. Initial algebras and terminal coalgebras: a survey. Preliminary version, 2010. URL:
  2. J. Adamek and J. Rosicky. Locally Presentable and Accessible Categories. Cambridge Tracts in Mathematics. Cambridge University Press, 1994. URL:
  3. F. Bartels. On generalised coinduction and probabilistic specification formats. PhD thesis, CWI, Amsterdam, April 2004. Google Scholar
  4. Henning Basold, Damien Pous, and Jurriaan Rot. Monoidal company for accessible functors (full version, with proofs). URL:
  5. Filippo Bonchi, Matias Lee, and Jurriaan Rot. Bisimilarity of open terms in stream GSOS. In FSEN, 2017. To appear. Google Scholar
  6. Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. Coinduction up-to in a fibrational setting. In CSL-LICS, pages 20:1-20:9. ACM, 2014. URL:, URL:
  7. Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59 of Cambridge Tracts in T.C.S. Cambridge University Press, 2016. URL:
  8. B. Klin. Bialgebras for structural operational semantics: An introduction. Theoretical Computer Science, 412(38):5043-5069, 2011. URL:
  9. Bartek Klin and Beata Nachyla. Presenting morphisms of distributive laws. In CALCO, volume 35 of LIPIcs, pages 190-204. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL:
  10. B. Knaster. Un théorème sur les fonctions d'ensembles. Annales de la Société Polonaise de Mathématiques, 6:133-134, 1928. Google Scholar
  11. Marina Lenisa, John Power, and Hiroshi Watanabe. Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads. Electronic Notes in Theoretical Computer Science, 33:230-260, 2000. URL:
  12. S. MacLane. Categories for the working mathematician. Springer, 1998. Google Scholar
  13. M. Makkai and R. Paré. Accessible Categories: The Foundations of Categorical Model Theory, volume 104 of Contemporary mathematics - American Mathematical Society. American Mathematical Society, 1989. Google Scholar
  14. Joachim Parrow and Tjark Weber. The largest respectful function. Logical Methods in Computer Science, 12(2), 2016. URL:
  15. Damien Pous. Complete lattices and up-to techniques. In APLAS, volume 4807 of LNCS, pages 351-366. Springer, 2007. URL:
  16. Damien Pous. Coinduction all the way up. In LICS, pages 307-316. ACM, 2016. URL:
  17. Damien Pous and Jurriaan Rot. Companions, codensity and causality. In FoSSaCS, volume 10203 of LNCS, pages 106-123, 2017. URL:
  18. John Power and Hiroshi Watanabe. Combining a monad and a comonad. Theoretical Computer Science, 280(1-2):137-162, 2002. URL:
  19. Jan J. M. M. Rutten. A coinductive calculus of streams. Mathematical Structures in Computer Science, 15(1):93-147, 2005. URL:
  20. Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing determinization from automata to coalgebras. Logical Methods in Computer Science, 9(1), 2013. URL:
  21. Ross Street. The formal theory of monads. J. of Pure and Applied Algebra, 2(2):149-168, 1972. URL:
  22. A. Tarski. A Lattice-Theoretical Fixpoint Theorem and its Applications. Pacific Journal of Mathematics, 5(2):285-309, June 1955. Google Scholar
  23. D. Turi and G. D. Plotkin. Towards a mathematical operational semantics. In LICS, pages 280-291. IEEE, 1997. URL:
  24. Hiroshi Watanabe. Well-behaved translations between structural operational semantics. Electronic Notes in Theoretical Computer Science, 65(1):337-357, 2002. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail