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.
翻译:我们将归纳数据类型理论与泛测量理论相结合。通过这种结合,我们发现许多自函子代数范畴实际上在同自函子的余代数范畴上得到丰富。这种丰富性通过测量余代数捕捉了所有可能的偏代数同态。因此,这一丰富范畴蕴含的信息比仅捕捉全代数同态的通常代数范畴更为丰富。我们利用初始代数概念的推广,在初始代数之外指定了新的代数。