Containers are used to carve out a class of strictly positive data types in terms of shapes and positions. They can be interpreted via a fully-faithful functor into endofunctors on Set. Monadic containers are those containers whose interpretation as a Set functor carries a monad structure. The category of containers is closed under container composition and is a monoidal category, whereas monadic containers do not in general compose. In this paper, we develop a characterisation of distributive laws of monadic containers. Distributive laws were introduced as a sufficient condition for the composition of the underlying functors of two monads to also carry a monad structure. Our development parallels Ahman and Uustalu's characterisation of distributive laws of directed containers, i.e. containers whose Set functor interpretation carries a comonad structure. Furthermore, by combining our work with theirs, we construct characterisations of mixed distributive laws (i.e. of directed containers over monadic containers and vice versa), thereby completing the 'zoo' of container characterisations of (co)monads and their distributive laws. We have found these characterisations amenable to development of existence and uniqueness proofs of distributive laws, particularly in the mechanised setting of Cubical Agda, in which most of the theory of this paper has been formalised.

翻译：容器用于通过形状和位置来刻画一类严格正数据类型。它们可以通过一个完全忠实的函子解释为集合上的自函子。单子容器是指那些作为集合函子的解释携带单子结构的容器。容器的范畴在容器复合下封闭且构成幺半范畴，而单子容器通常不能复合。本文发展了单子容器分配律的表征方法。分配律最初是作为两个单子底层函子的复合也能携带单子结构的充分条件而提出的。我们的工作与Ahman和Uustalu对定向容器（即其集合函子解释携带余单子结构的容器）分配律的表征研究相平行。此外，通过将我们的工作与他们的研究相结合，我们构建了混合分配律（即定向容器对单子容器及其反向情形）的表征，从而完善了（余）单子及其分配律的容器表征"动物园"。我们发现这些表征特别适用于分配律存在性与唯一性证明的构建，尤其是在Cubical Agda的机械化验证环境中——本文大部分理论已在该环境中完成形式化验证。