Category theory has had a profound effect on modern mathematics. Over the years, is has become an indispensible tool in algebra, topology, computer science, logic and even physics. Moreover, it has been recognized for some time that the theory of higher categories is intimately connected to some of the most promising lines of modern mathematical research: topological quantum field theory, derived algebraic geometry, stable homotopy theory, quantum groups and more. And with the introduction of Univalent Type Theory by Voevodsky in 2009, we can add logic, computer science and constructive mathematics to that list as well1.

This site is dedicated to a certain approach to the theory of higher categories based on a collection of shapes called the opetopes. It is probably fair to say that among the currently available approaches to higher category theory, the opeoptic one is the among least well known. This is not without some justification: indeed, finding a sufficiently rigorous definition of the opetopes has occupied a number of different authors, and the subtleties involved might leave one with the impression that the approach is more trouble than it is worth.

Perhaps another reason for the perceived difficulty of the opetopes can be seen in the table below:

Cell Type In Dimension 2 In Higher Dimensions
Globular Circle Spheres
Simplicial Triangle Simplices
Cubical Square Cubes
Opetopic (Planar) Tree N-Trees

While the more direct approaches to higher category theory employ cells based on shapes which are exceedingly familiar even in higher dimensions, the higher dimensional analogs of trees are perhaps less so. Moreover, there is some flexibility in what exactly we mean by higher dimensional tree, and the opetopes can be seen as a class of particularly well behaved ones. All the subtleties in the definition of these objects are involved in making precise what one means by "well-behaved".

Why Opetopes?

So, then, what makes the opetopes worth the effort?

To begin to answer that question, let me first observe that one of the hallmarks of category theory is the use of diagrammatic reasoning, namely, the use of commutative diagrams to express equations. Whatever ontological status we grant to these diagrams, it is difficult to deny their pragmatic value: it is often times simply more efficient to draw a well conceived commutative diagram than to explicitly list a collection of equations among maps.

As we pass to higher categories, finding reasonable diagrammatic representations becomes more challenging. Certainly the literature on 2-categories has a well developed system of notation for two-cells, but what about beyond that? Are we stuck?

On this site, we will be developing a systematic way of representing and manipulating "opetopic diagrams", and the central thesis can be summarized as follows:

Opetopic diagrams provide an elementary formal account of diagrammatic reasoning which remains valid in all dimensions.

So whereas other approaches benefit from their simplicity on the semantic side, the opetopic approach benefits from its diversity on the syntactic side.


Of course, the relationship between higher categorical thinking and constructive mathematics was well known, or at least implicit, long before the recent advancements in type theory. But certainly the introduction of univalent ideas have contributed to a deepening of our understanding of the connection.