Directed Containers as Categories

Danel Ahman
Tarmo Uustalu

Directed containers make explicit the additional structure of those containers whose set functor interpretation carries a comonad structure. The data and laws of a directed container resemble those of a monoid, while the data and laws of a directed container morphism those of a monoid morphism in the reverse direction. With some reorganization, a directed container is the same as a small category, but a directed container morphism is opcleavage-like. We draw some conclusions for comonads from this observation, considering in particular basic constructions and concepts like the opposite category and a groupoid.

In Robert Atkey and Neelakantan Krishnaswami: Proceedings 6th Workshop on Mathematically Structured Functional Programming (MSFP 2016), Eindhoven, Netherlands, 8th April 2016, Electronic Proceedings in Theoretical Computer Science 207, pp. 89–98.
Published: 1st April 2016.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: