Higher-order many-sorted categorial algebras via generalized hep-derivors

Abstract

Higher-order many-sorted categorial algebras are many-sorted algebras whose carriers are strict higher-order categories and whose operations are higher-order functors. They admit a homogeneous and a heterogeneous presentation, both by partial algebras whose operation domains are given by existence equations. To relate these presentations and their dimensions, we introduce generalized hep-derivors between hierarchical equationally partial signatures. A generalized hep-derivor selects carriers by existence equations in one variable and interprets operation symbols by terms, with operation domains evaluated recursively in the transformed algebra. Every generalized hep-derivor induces a functor between categories of many-sorted partial algebras. The values of this functor satisfy the domain conditions wherever their operations are defined, and we characterize when the operations are defined exactly where these conditions hold. The functor induced by a composite receives a natural inclusion from the composite of the induced functors; this inclusion, which can be strict, makes the induced functors a normal lax indexed category. In finite dimensions, generalized hep-derivors realize graduation and unification as an equivalence between the homogeneous and heterogeneous presentations, and discretization as a left adjoint to truncation. In dimension $ω$, we reconstruct the categories of $ω$-categorial algebras as projective limits of their finite-dimensional truncations and obtain unification by a quotient construction; we also establish algebraic squares and compatibility with change of signature. Finally, for nonempty sets of sorts, we show that the finite-dimension condition in the homogeneous $ω$-presentation is not axiomatizable by quasi-existence equations on its fixed signature.