  This ongoing project aims to define and investigate, from the standpoint of
category theory, order theory and universal algebra, the notions of
higher-order many-sorted rewriting system and of higher-order many-sorted
categorial algebra and their relationships, via the higher-order Curry-Howard
isomorphisms.
  The ultimate goal, to be developed in future versions of this work, is to
define and investigate the category of towers, whose objects will consist of
families, indexed by $\mathbb{N}$, of higher-order many-sorted rewriting
systems and of higher-order many-sorted categorial algebras, including
higher-order Curry-Howard type results for the latter, together with an
additional structure that intertwines such $\mathbb{N}$-families; and whose
morphism from a tower to another will be families, indexed by $\mathbb{N}$, of
morphisms between its higher-order many-sorted rewriting systems and of
higher-order many-sorted categorial algebras compatible with their structures.
All feedback is appreciated.
