Monoidal bicategories, linear logic and operads

When we begin to study mathematics, we learn that the operation of multiplication on numbers satisfies some basic rules. One of these rules, known as associativity, says that for any three numbers a, b and c, we get the same result if we multiply a and b and then multiply the result by c or if we multiply a by the result of multiplying b and c. This leads to the abstract algebraic notion of a monoid, which is a set (in this case the set of natural numbers) equipped with a binary operation (in this case multiplication) that is associative and has a unit (in this case the number 1).

If we continue to study mathematics, we encounter a new kind of multiplication, no longer on numbers but on sets, which is known as Cartesian product. Given two sets A and B, their Cartesian product is the set A x B whose elements are the ordered pairs (a, b), where a is an element of A and b is an element of B. Pictorially, the Cartesian product of two sets is a grid with coordinates given by the elements of the two sets. This operation satisfies some rules, analogous to those for the multiplication of numbers, but a little more subtle. For example, if we are given three sets A, B and C, then the set A x (B x C) is isomorphic (rather than equal) to the set (A x B) x C. Here, being isomorphic means that we they are essentially the same by means of a one-to-one correspondence between the elements A x (B x C) and those of (A x B) x C. This construction leads to the notion of a monoidal category, which amounts to a collection of objects and maps between them (in this case the collection of all sets and functions between them) equipped with a multiplication (in this case the Cartesian product) that is associative and has a unit (in this case the one-element set) up to isomorphism. Monoidal categories, introduced in the '60s, have been extremely important in several areas of mathematics (including logic, algebra, and topology) and theoretical computer science. In logic and theoretical computer science, they connect to linear logic, in which one keeps track of the resources necessary to prove a statement.

This project is about the next step in this sequence of abstract notions of multiplication, which is given by the notion of a monoidal bicategory. In a bicategory, we have not only objects and maps but also 2-maps, which can be thought of as "maps between maps" and allow us to capture how different maps relate to each other. In a monoidal bicategory, we have a way of multiplying their objects, maps and 2-maps, subject to complex axioms. Monoidal bicategories, introduced in the '90s, have potential for applications even greater than that of monoidal categories, as they allow us to keep track of even more information.

We seek to realise this potential by advancing the theory of monoidal bicategories. We will prove fundamental theorems about them, develop new connections to linear logic and theoretical computer science and investigate examples that are of interest in algebra and topology. Our work connects to algebra via an important research programme known as "categorification", which is concerned with replacing set-based structures (like monoids) with category-based structures (like monoidal categories) in order to obtain more subtle invariants. Our work links to topology via the notion of an operad, which is a flexible tool used to describe algebraic structures in which axioms do not hold as equalities, but rather up to weak forms of isomorphism. Overall, this project will bring the theory of monoidal bicategories to a new level and promote interdisciplinary research within mathematics and with theoretical computer science.

The proposed research has potential impact to the software industry by benefitting researchers working on the design and implementation of new programming languages and software verification systems. In these areas, it important to have methods to write computer programs that are computationally feasible, i.e. do not use too many resources (e.g. time and memory), and are provably correct (i.e. are guaranteed not to contain any bugs). Both are important issues from a practical point of view, as inefficient or incorrect programs can cause loss of life and money.

Our research will benefit researchers in these areas via the work on linear type theories. Indeed, linear type theories have long been known to provide a good setting for the design of programming languages with control over the computational resources used in programs. Our work will provide a new class of linear type theories with additional features and constructs not considered in combination yet, such as differentiation, trace and explicit substitutions. These lead to very expressive programming languages, which enable users to write programs more elegantly and efficiently. Our work will also ensure the soundness of the programs written in these languages since it provide models for these linear type theories.

Our work will also be beneficial for new generations of computer systems based for the verification of software and formalisation of mathematics, as some of the features of our linear type theories may be included in those systems, as a way of controlling complexity of programs and proofs.

We will ensure that our work achieves the maximal potential impact with an energetic activity of dissemination of our work beyond pure mathematics, by interacting with the research communities in programming language and verification, by working with our Project Partner David Spivak on applications of category theory to software engineering and by presenting our work also in conferences in theoretical computer science and applied category theory.