Free algebras of topologically enriched multi-sorted equational theories
share
Classical multi-sorted equational theories and their free algebras have been fundamental in mathematics and computer science. In this paper, we present a generalization of multi-sorted equational theories from the classical (Set-enriched) context to the context of enrichment in a symmetric monoidal category V that is topological over Set. Prominent examples of such categories include: various categories of topological and measurable spaces; the categories of models of relational Horn theories without equality, including the categories of preordered sets and (extended) pseudo-metric spaces; and the categories of quasispaces (a.k.a. concrete sheaves) on concrete sites, which have recently attracted interest in the study of programming language semantics. Given such a category V, we define a notion of V-enriched multi-sorted equational theory. We show that every V-enriched multi-sorted equational theory T has an underlying classical multi-sorted equational theory |T|, and that free T-algebras may be obtained as suitable liftings of free |T|-algebras. We establish explicit and concrete descriptions of free T-algebras, which have a convenient inductive character when V is cartesian closed. We provide several examples of V-enriched multi-sorted equational theories, and we also discuss the close connection between these theories and the presentations of V-enriched algebraic theories and monads studied in recent papers by the author and Lucyshyn-Wright.
READ FULL TEXT