We combine the theory of inductive data types with the theory of universal measurings. By doing so, we find that many categories of algebras of endofunctors are actually enriched in the corresponding category of coalgebras of the same endofunctor. The enrichment captures all possible partial algebra homomorphisms, defined by measuring coalgebras. Thus this enriched category carries more information than the usual category of algebras which captures only total algebra homomorphisms. We specify new algebras besides the initial one using a generalization of the notion of initial algebra.
翻译:我们将归纳数据类型理论与通用度量理论结合起来,发现许多代数自函子范畴实际上富有相应自余函子范畴,富集了通过测量自余代数所定义的所有可能的部分代数同态。因此,这个富集范畴携带比仅捕获总代数同态的常规代数范畴更多的信息。我们使用初始代数的推广指定了新的代数。