Monoid Structures on Indexed Containers

Abstract

Containers represent a wide class of type constructions that are relevant for functional programming and (co)inductive reasoning. Indexed containers generalize this notion to better fit the scope of dependently typed programming. When interpreting types to be sets, a container describes an endo functoron the category of sets while an I-indexed container describes an endo functor on the category SetI of I-indexed families of sets. We consider the monoidal structure on the category of I-indexed containers whose tensor product of containers describes the composition of the respective induced endofunctors. We then give a combinatorial characterization of monoids in this monoidal category, and we show how these monoids correspond precisely to monads on the induced endofunctors on SetI. Lastly, we conclude by presenting some examples of monads on SetI that fall under our characterization, including the product of two monads, indexed variants of the state and the writer monads and an example of a free monad. The technical results of this work are accompanied by a formalization in the proof assistant Cubical Agda.