In this article, we combine Sweedler's classic theory of measuring coalgebras -- by which $k$-algebras are enriched in $k$-coalgebras for $k$ a field -- with the theory of W-types -- by which the categorical semantics of inductive data types in functional programming languages are understood. In our main theorem, we find that under some hypotheses, algebras of an endofunctor are enriched in coalgebras of the same endofunctor, and we find polynomial endofunctors provide many interesting examples of this phenomenon. We then generalize the notion of initial algebra of an endofunctor using this enrichment, thus generalizing the notion of W-type. This article is an extended version of arXiv:2303.16793, it adds expository introductions to the original theories of measuring coalgebras and W-types along with some improvements to the main theory and many explicitly worked examples.
翻译:本文结合了Sweedler关于测量余代数的经典理论——通过该理论,$k$-代数在域$k$的余代数中得以丰富——与W-类型的理论——通过该理论,函数式编程语言中归纳数据类型的范畴语义得以理解。在我们的主要定理中,我们发现某些假设下,自函子的代数可在同一自函子的余代数中丰富化,并且发现多项式自函子为此现象提供了许多有趣的示例。随后,我们利用这种丰富化推广了自函子初始代数的概念,从而推广了W-类型的定义。本文是arXiv:2303.16793的扩展版本,增加了对测量余代数和W-类型原始理论的阐释性介绍,同时对主要理论进行了若干改进,并提供了大量详细演算的示例。