nLab polynomial comonad

Definition

A polynomial comonad on a category is a comonad whose underlying endofunctor is a polynomial functor.

Properties

• A polynomial comonad on Set is equivalent to a small category (Ahman-Uustalu, 2016).

• A morphism of polynomial comonads on $\mathrm{Set}$ is equivalent to a retrofunctor (Ahman-Uustalu, 2017).

• A two-sided comodule $A \nrightarrow B$ between polynomial comonads on $\mathrm{Set}$, viewed as small categories, is equivalent to a parametric right adjoint $[A, \mathrm{Set}] \rightarrow [B, \mathrm{Set}]$ between functor categories (Garner, 2019).

References

Polynomial comonads were first studied under the name directed containers in:

• Danel Ahman, James Chapman, Tarmo Uustalu, When is a container a comonad?, Logical Methods in Computer Science 10 3 (2014) 1-48 [arXiv:1408.5809, doi:10.2168/LMCS-10(3:14)2014]

The equivalence between polynomial comonads on $\mathrm{Set}$ and small categories was shown in:

• Danel Ahman, Tarmo Uustalu, Directed Containers as Categories, EPTCS 207 (2016) 89-98 [arXiv:1604.01187, doi:10.4204/EPTCS.207.5]

The observation that morphisms of polynomial comonads are the same as retrofunctors (under the name cofunctor) appears in:

• Danel Ahman, Tarmo Uustalu, Taking updates seriously, CEUR Workshop Proceedings 1827 (2017) 59-73 [PDF]

The notion of (two-sided) comodule between polynomial comonads was given in:

• Richard Garner, Polynomial comonads and comodules, HoTTEST Seminar (2019) [slides, video]

A detailed study of polynomial comonads and their morphisms appears in Chapter 7 of the (unpublished) book:

• Nelson Niu, David Spivak, Polynomial Functors: A Mathematical Theory of Interaction, draft (2023) [arXiv:2312.00990]