A computational approach to higher categories

Abstract

Higher categories have become an important tool in mathematics, computer science, and physics. String diagrams provide an intuitive way for working with higher categories and have seen a surge of interest in recent years. However, in practice, they can be hard to draw or manipulate, and there is a need for tools that can help with this. In this thesis, we describe a proof assistant called homotopy.io for working with higher categories using string diagrams, or more generally, manifold diagrams. It implements the theory of associative n-categories, which is a semistrict model of higher categories. The terms of the theory, called n-diagrams, are defined inductively and have a direct representation as manifold diagrams. The tool allows users to construct and manipulate n-diagrams, and visualise them in up to four dimensions as string diagrams (in 2D), surface diagrams (in 3D), or smooth animations of surface diagrams (in 4D). The main contribution of this thesis is the development of two key components of the proof assistant, as well as the novel categorical concepts that underpin them. First, we have the layout algorithm, which is used to obtain the optimal rendering coordinates of the vertices of n-diagrams and is crucial for their visualisation. This works by generating a system of linear constraints using a new categorical construction called injectification. Second, we have anticontraction, which is a method for constructing homotopies between n-diagrams that increase the local complexity. This is based on a new categorical notion of anticolimits which provide a way to decompose an object into a colimit of other objects. Moreover, we show that the category of partially ordered sets is the free conservative cocompletion of the category of finite (non-empty) totally ordered sets. Although this is a self-contained result, it also motivates the use of posets in layout and anticontraction.