You may wonder what is monoidal topology and why it should be something interesting for computer scientists (theoretical ones, at least). In a slogan, monoidal topology is a unifying theory of ordered, metric and topological spaces. Such unification is made possible by the non-trivial observation that the above three notions can be ‘reduced’ to specific categorical structures.
What Is Monoidal Topology?
Monoidal topology is built over the fundamental work of Lawvere and Barr. In his 1973 paper Metric Spaces, Generalized Logic, and Closed Categories Lawvere showed that the notions of metric space, ordered set and (small) category are all instances of the more general notion of enriched category, thus strengthening his theory that fundamental structures are themselves categories.
Three years before, in his paper Relational Algebras, Barr extended the work of Manes, characterising topological spaces as lax algebras in the category of sets and relation for the ultrafilter monad (thus fully exploiting the algebraic nature of topological spaces).
This is all very nice, but the math behind those stories is not always trivial, and in general it is not part of the background of a computer scientist or a logician (it requires some knowledge of topology, order theory and category theory). The main reference for this subject (Monoidal Topology. A Categorial Approach to Order Metric, and Topology, edited by Hofmann, Seal and Tholen) is an excellent book, but it is de facto targeted to mathematicians. This doesn’t mean that it is not a good reading for logicians or computer scientists (quite the contrary!) , it just means that in order to fully appreciate the technical materials in it (and to get the ‘big picture’) the reader is the required to have some specific mathematical background.
That was at least my experience: I had background in order theory and basic category theory, but I never studied neither topology nor non-entry level category theory. This is the main reason why I decided to write this series of blog post: to provide an accessible introduction to the fascinating subject of monoidal topology targeted to students and researchers in Logic and Computer Science.
Why is Monoidal Topology Relevant for Computer Science?
I was introduced to Barr’s work by Paul Levy last winter, in the context of a research project on behavioural equivalences for -calculi. The notion of lax extension of a monad turned out to be fundamental in our work. Since then I started working on extending our results from behavioural equivalences to behavioural metrics (which is my current research topic), and at the same time I studied the development of Barr’s work. The former directly led me to the work of Lawvere on metric spaces, ordered sets, and small categories, whereas the latter led me to monoidal topology (which turned out to generalise the Lawvere’s work).
In the end, I reached the conclusion that monoidal topology provides the right environment to study behavioural equivalences and metrics for functional languages. But it can actually do more. Much more! For instance, it finds nice applications in coalgebra, logic and denotational semantics (as I will discuss in the second part of this series).