The initial release of Globular works best in the Chrome browser. For discussion, go to the nForum thread.
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 homotopy.io.
If you would like to cite Globular, you can use the BiBTeX entry
@InProceedings{
globular,
author={Krzysztof Bar and Aleks Kissinger and Jamie Vicary},
title={Globular: an online proof assistant for higher-dimensional rewriting},
note={\href{http://ncatlab.org/nlab/show/Globular}{ncatlab.org/nlab/show/Globular}},
pages={34:1--34:11},
volume=52,
year=2016,
booktitle={Leibniz International Proceedings in Informatics}}
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.)
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 $S$ and $T$, 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)$ and $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+1$ act on $n$-diagrams by rewriting, replacing a subdiagram of shape $S$ and replacing it with a subdiagram of shape $T$.
The only things that Globular understands are $k$-cells, for some value of $k$. So if you want to build an $n$-category where an equation $f=g$ holds between $n$-cells, you have to do it by adding $(n+1)$-cells $a:f \to g$ and $b:g \to f$. If you then build some composite $C[f]$ involving $f$, you can apply the cell $a$ to obtain $C[g]$, and we interpret this as the equation $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 globular.science 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.
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 $D$ is $k$-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!
Globular can currently present string-diagram visualizations of 0-, 1- and 2-dimensional diagrams. Viewing a $k$-dimensional diagram for $k \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.)
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 $n$-category, a $p$-cell and an $q$-cell can be composed in $\text{min}(p,q)$ different directions: along a common boundary 0-cell, or 1-cell, and so on, up to a common boundary $(\text{min}(p,q)-1)$-cell.
In Globular, composition works differently: a $p$-cell and a $q$-cell can be composed in just one way: along a common boundary $(\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 $n$-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,q$ and every $0 \leq n \lt \text{min}(p,q)$—there exists a $(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 $n$-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 $n$-category, you may need to make use of every type of $k$-category singularity for $k \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 $n$-cells along a common boundary $(n-2)$-cell.
Interchangers
$\mathraisebox{1.8cm}{\to}$ $\qquad\qquad$
Naturality of the interchanger in one variable
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
A $k$-cell $f:A \to B$ in an $\infty$-category is invertible when there is an inverse cell $f ^{-1} : B \to A$, and invertible $(k+1)$-cells $\mu: \mathrm{id}_A \to f ^{-1} \circ f$ and $\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 $k$-cell, and where ‘.’ is forward composition of $k$-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 $D$ be the current diagram, which is $k$-dimensional, and let $s(D)$ and $t(D)$ be its source and target $(k-1)$-diagrams. Then the theorem command command creates two new generators:
The generator $T$ can be used in future proofs to ‘stand in’ for the diagram $D$. At any point, the generator $P$ can be used to replace $T$ with the content of diagram $D$. Since $P$ is invertible, it could also be used to identify $D$ as a subdiagram of a larger proof, and replace it with $T$, 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 $k$-dimensional cell in an $n$-dimensional diagram, $(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 $n$-diagram is defined in the following way. An $n$-cell at height $y$ has coordinate $[y]$. A $k$-cell for $k \lt n$ has leading coordinate given by its height $z$ in the diagram, and subsequent coordinates given by its coordinates in the slice diagram at that height.
based on plain type theory/set theory:
based on dependent type theory/homotopy type theory:
For monoidal category theory:
projects for formalization of mathematics with proof assistants:
Archive of Formal Proofs (using Isabelle)
ForMath project (using Coq)
UniMath project (using Coq)
Xena project (using Lean)
Historical projects that died out:
Krzysztof Bar, Aleks Kissinger, Jamie Vicary, Globular: an online proof assistant for higher-dimensional rewriting, arXiv:1612.01093
Jamie Vicary, Globular tutorial video, 2015-12-07 15 minute video
Jamie Vicary, Data Structures for Quasistrict Higher Categories, referencing arxiv:1610098, 2016-12-05 talk at Simons Institute 48 minute video