标题： 索引容器上的独异点结构 显示英文标题

标题： Monoid Structures on Indexed Containers

摘要： 容器代表了一类广泛的类型构造，对于函数式编程和(共)归纳推理具有重要意义。 索引容器将这一概念推广，以更好地适应依赖类型编程的范围。 当将类型解释为集合时，容器描述了集合范畴上的自函子，而I-索引容器描述了I-索引集合族范畴Set^I上的自函子。 我们考虑I-索引容器范畴上的张量积结构，其中容器的张量积描述了相应诱导自函子的复合。 然后，我们给出了这个张量范畴中乘法结构的组合特征，并展示了这些乘法结构如何精确对应于Set^I上诱导自函子的单子。 最后，我们通过展示一些符合我们特征的Set^I上的单子示例来结束，包括两个单子的乘积、状态和写入单子的索引变体以及一个自由单子的示例。 这项工作的技术结果伴随着在证明助手Cubical Agda中的形式化。 显示英文摘要

摘要： Containers represent a wide class of type constructions 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 endofunctor on the category of sets while an I-indexed container describes an endofunctor on the category Set^I 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 Set^I. Lastly, we conclude by presenting some examples of monads on Set^I 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.