Higher category theory

higher category theory

Basic concepts

Basic theorems





Universal constructions

Extra properties and structure

1-categorical presentations

The initial release of Globular works best in the Chrome browser. For discussion, go to the nForum thread.


Globular screenshot



Globular is a web-based proof assistant for finitely-presented semistrict globular higher categories. It allows one to formalize higher-categorical proofs in finitely-presented n-categories, visualize them as string diagrams, and share them with collaborators, or with the world. It is available at this address:

We recommend the Chrome browser.

Globular currently operates up to the level of 4-categories. By the yoga of k-tuply monoidal n-categories, this also allows one to construct proofs in the following settings:

The model of semistrict higher categories that Globular uses puts all the weak structure in the interchangers, and higher associated structures. At the level of 3-categories, Globular implements the axioms of a Gray category; since every tricategory is known to be equivalent to a semistrict 3-category, this means that any algebraic proof in a finitely-presented tricategory can be formalized. At the level of 4-categories, this is an implementation of a new definition of semistrict 4-category which is not yet published, and for which it is conjectured that every weak 4-category is equivalent to a semistrict 4-category.

Globular is free to use, and open-source. There is a lot to be done, on both a theoretical and practical level, and anybody can get involved with development. If you are interested, please get in touch with Jamie Vicary. Globular has been developed in the Quantum Group of the Department of Computer Science at the University of Oxford, by Krzysztof Bar, Katherine Casey, Aleks Kissinger, Jamie Vicary and Caspar Wylie.

If you’ve never used Globular before, the tutorial video is a good place to start. To report a bug, please use the issue tracker.

We are extremely grateful to John Baez, Manuel Bärenz, Bruce Bartlett, Eugenia Cheng, Chris Douglas, Eric Finster, Nick Gurski, André Henriques, Samuel Mimram and Dominic Verdon for useful discussions.

Globular will soon followed by a successor tool

If you would like to cite Globular, you can use the BiBTeX entry

  author={Krzysztof Bar and Aleks Kissinger and Jamie Vicary}, 
  title={Globular: an online proof assistant for higher-dimensional rewriting}, 
  booktitle={Leibniz International Proceedings in Informatics}}

Example proofs

To see what can be done with Globular, look at these example proofs. To navigate through them, use the Project and Slice controls in the top-right of the main diagram (see Changing the view.)

Basic functionality


Signatures and diagrams. Using Globular involves two main techniques: building the signature, and building a diagram over the signature. The signature is the list of cells that are available, and the diagram is a particular composite of those cells. A diagram can be thought of as a composite cell in the free semistrict \infty-category generated by the signature.

The signature can be enlarged by building diagrams SS and TT, and assigning them in turn as the source and target of a new cell, using the ‘Source’ and ‘Target’ buttons in the menu on the right of the interface. Any pair of diagrams can be chosen which satisfy the globularity conditions s(S)=s(T)s(S) = s(T) and t(S)=t(T)t(S) = t(T). The new cell can then be given a name and a colour, to make it easy to identify.

Diagrams are built by clicking on cells of the signature, and by clicking and dragging on the diagram itself. Signature cells of dimension n+1n+1 act on nn-diagrams by rewriting, replacing a subdiagram of shape SS and replacing it with a subdiagram of shape TT.

The only things that Globular understands are kk-cells, for some value of kk. So if you want to build an nn-category where an equation f=gf=g holds between nn-cells, you have to do it by adding (n+1)(n+1)-cells a:fga:f \to g and b:gfb:g \to f. If you then build some composite C[f]C[f] involving ff, you can apply the cell aa to obtain C[g]C[g], and we interpret this as the equation C[f]=C[g]C[f]=C[g]. In a slogan, this is equality via rewriting. This is consistent with the basic premise of homotopy type theory: treat your proofs as first-order structures, which can themselves be reasoned about directly.

Accounts. If you create an account on the site, you can save workspaces to your private account, and resume work on them when you log back in to your account from any computer. You can also click ‘Share’, which shares a workspace privately with another user, and ‘Publish’, which creates a permanent public version of your workspace that can be linked to from a research paper, or from elsewhere on the web.

Export and import. Use the ‘Export’ feature to download a copy of your workspace to your local machine, and ‘Import’ to upload a previously-download workspace. This functionality only involves your browser, not the server, so you do not need to log in or even create an account to use these features. If you import a workspace, log in, and click ‘Save’, then a copy of the imported workspace will be saved to the server.

Security and privacy. The plain text of your password is not stored on the server. However, your private workspaces are saved in plain text, and as such should not be considered highly secure, as they could be accessed by someone with site administrator credentials. The administrators pledge not to access any user data, except from the registered email address, without the permission of that individual user. In other words: your private work is private! User data is backed up nightly to a secure server.

Manipulating diagrams

A diagram is a composite of the cells in the current signature, and basic diagram manipulation can be performed by clicking on the signature, as follows, where we suppose our diagram DD is kk-dimensional.

The menu on the right-hand side of the screen gives further commands. Each of these commands has a shortcut key, which is also given.

Also, the user can click and click-and-drag on the diagram to produce various effects. When a command is ambiguous, a menu will be presented to allow the user to choose their preferred action.

Clicking and dragging is designed to work as if you were really ‘touching’ the strings. So if you want to braid one strand over another, click the strand to ‘grab’ it, and ‘pull’ it to one side. If you want to pull a vertex through a braiding, click the vertex to ‘grab’ it, and ‘pull’ it up or down through its adjacent braiding. Of course, Globular will only carry out the command if the move you are attempting to make is actually valid in that location.

The most common move to perform is a basic interchanger, where two unrelated critical points with adjacent heights have their heights exchanged. Holding the Shift button while clicking-and-dragging tells Globular to only look for basic interchanger moves. This speeds up the processing, and is particularly useful for applying long chains of interchangers.

In order to undo any change then click the back button in your browser. This feels very counter-intuitive but trust me it works!

Changing the view

Globular can currently present string-diagram visualizations of 0-, 1- and 2-dimensional diagrams. Viewing a kk-dimensional diagram for k>2k \gt 2 is made possible by projection and slicing, controlled by number scrollers which appear in the top-right of a diagram.

You can also zoom the main diagram using the scroll wheel of your mouse, and scroll around by clicking-and-dragging with the right mouse button (on a Mac trackpad, this is a two-fingered press-hard-and-drag. Yes, this really is a thing. If it doesn’t seem to work, you’re not pressing hard enough—the trackpad should ‘click’ under your fingers.)

Technical implementation details

Globular is written in Javascript, and performs all its computations client-side, in the browser. Most of the computations it has to perform are linear in the size of the diagram, so this is quite computationally feasible, even for large proofs. The back-end is a Node.js server that allows the saving, sharing and publishing of workspaces. Graphics are implemented in SVG. Project data is compressed using the LZ4 algorithm.



In a 2-category, a 1-cell and a 2-cell can be composed in one direction (horizontal composition), and two 2-cell can be composed in two directions (horizontal and vertical composition.) In general, in a traditional globular nn-category, a pp-cell and an qq-cell can be composed in min(p,q)\text{min}(p,q) different directions: along a common boundary 0-cell, or 1-cell, and so on, up to a common boundary (min(p,q)1)(\text{min}(p,q)-1)-cell.

In Globular, composition works differently: a pp-cell and a qq-cell can be composed in just one way: along a common boundary (min(p,q)1)(\text{min}(p,q)-1)-cell. The reason for this design decision is that in terms of the graphical calculus, of all the different composites that an ordinary globular nn-category allows, this is the only composition that results in a diagram in generic position. Nothing is lost by this restriction, since (conjecturally) the other composites can be recovered up to isomorphism by whiskering, in just the same way that horizontal composition of 2-cells in a 2-category can be expressed in terms of vertical composites and whiskering of 2-cell by identity 1-cell.

For every way that Globular doesn’t let you compose cells—that is, for every p,qp,q and every 0n<min(p,q)0 \leq n \lt \text{min}(p,q)—there exists a (p+qn1)(p+q-n-1)-cell, which resolves the singularity that would be created if this composite were actually formed. These singularity resolutions manifest in Globular as higher-dimensional cells, which allow parts of a diagram to move around each other; using them effectively is a key part of formalizing higher-dimensional proofs. The main difficulty in the definition of semistrict nn-categories is describing these structures.

In this section we list the singularities which Globular recognizes. We organize them by categorical dimension, because to formalize a proof in an nn-category, you may need to make use of every type of kk-category singularity for knk \leq n. Also, you can add any fixed natural number to the dimensions involved to get higher-dimensional versions of the same singularities; for example, interchangers arise as the composite of two nn-cells along a common boundary (n2)(n-2)-cell.

2-category singularities


Interchanger source \mathraisebox{1.8cm}{\to} Interchanger target \qquad\qquad Interchanger projection

3-category singularities

Naturality of the interchanger in one variable

4-category singularities

Naturality of naturality of the interchanger in one variable

Naturality of the interchanger in two variables

Naturality of invertibility of the interchanger

Contractible 3rd Reidemeisterators

Other features


A kk-cell f:ABf:A \to B in an \infty-category is invertible when there is an inverse cell f 1:BAf ^{-1} : B \to A, and invertible (k+1)(k+1)-cells μ:id Af 1f\mu: \mathrm{id}_A \to f ^{-1} \circ f and ν:id Bff 1\nu: \mathrm{id}_B \to f \circ f ^{-1}. This is a co-inductive definition, giving rise to an infinite amount of higher-dimensional structure.

In Globular, selecting the ‘Invertible’ option for a cell in the signature allows this higher structure to be used in diagrams, by clicking or clicking-and-dragging at a point of a diagram or its boundary. If more than one piece of higher invertible structure could be inserted at the location of the click, a menu is presented and the user can choose which is intended.

When you move your pointer over a diagram, a little label will pop up telling you what’s underneath the pointer. Doing this near a vertex, you will see that Globular isn’t really aware that the lines curve, so you will need to take care when clicking or clicking-and-dragging that Globular is correctly identifying the structure you are trying to interact with.

The labels are written using the following syntax, where ‘X’ is some arbitrary label denoting a kk-cell, and where ‘.’ is forward composition of kk-cells. Note that every comma increases the dimension by 1.

Note that interchangers are of dimension at least 3, and pull-throughs are of dimension at least 4.


The theorem command allows a diagram to be stored, in a such way that it can be reused as a component in subsequent diagrams. The idea is that the diagram is a ‘theorem’ proving that its source can be rewritten into its target. The ‘proof’ is the diagram itself.

Concretely, let DD be the current diagram, which is kk-dimensional, and let s(D)s(D) and t(D)t(D) be its source and target (k1)(k-1)-diagrams. Then the theorem command command creates two new generators:

The generator TT can be used in future proofs to ‘stand in’ for the diagram DD. At any point, the generator PP can be used to replace TT with the content of diagram DD. Since PP is invertible, it could also be used to identify DD as a subdiagram of a larger proof, and replace it with TT, making the larger proof easier to understand.


Composites produced by Globular are in generic position; for example, no two vertices ever appear at the same height. As a result, there is a simple coordinate system that can be used to refer to elements of a diagram. For a kk-dimensional cell in an nn-dimensional diagram, (nk+1)(n-k+1) coordinates must be provided; that is, the number of coordinates is the codimension of the cell, plus 1. Moving the mouse cursor over a diagram in the screen shows the coordinate of the element underneath the cursor.

The coordinate system for an nn-diagram is defined in the following way. An nn-cell at height yy has coordinate [y][y]. A kk-cell for k<nk \lt n has leading coordinate given by its height zz in the diagram, and subsequent coordinates given by its coordinates in the slice diagram at that height.

proof assistants:

based on plain type theory/set theory:

based on dependent type theory/homotopy type theory:

For monoidal category theory:

For higher category theory:

projects for formalization of mathematics with proof assistants:

Historical projects that died out: