\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{Globular}

[[!redirects globular]]

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{higher_category_theory}{}\paragraph*{{Higher category theory}}\label{higher_category_theory}

[[!include higher category theory - contents]]

\emph{The initial release of Globular works best in the Chrome browser. For discussion, go to the \href{http://nforum.ncatlab.org/discussion/6829/globular}{nForum thread}.}

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{introduction}{Introduction}\dotfill \pageref*{introduction} \linebreak
\noindent\hyperlink{overview}{Overview}\dotfill \pageref*{overview} \linebreak
\noindent\hyperlink{example_proofs}{Example proofs}\dotfill \pageref*{example_proofs} \linebreak
\noindent\hyperlink{basic_functionality}{Basic functionality}\dotfill \pageref*{basic_functionality} \linebreak
\noindent\hyperlink{overview_2}{Overview}\dotfill \pageref*{overview_2} \linebreak
\noindent\hyperlink{manipulating_diagrams}{Manipulating diagrams}\dotfill \pageref*{manipulating_diagrams} \linebreak
\noindent\hyperlink{changingtheview}{Changing the view}\dotfill \pageref*{changingtheview} \linebreak
\noindent\hyperlink{technical_implementation_details}{Technical implementation details}\dotfill \pageref*{technical_implementation_details} \linebreak
\noindent\hyperlink{singularities}{Singularities}\dotfill \pageref*{singularities} \linebreak
\noindent\hyperlink{overview_3}{Overview}\dotfill \pageref*{overview_3} \linebreak
\noindent\hyperlink{2category_singularities}{2-category singularities}\dotfill \pageref*{2category_singularities} \linebreak
\noindent\hyperlink{3category_singularities}{3-category singularities}\dotfill \pageref*{3category_singularities} \linebreak
\noindent\hyperlink{4category_singularities}{4-category singularities}\dotfill \pageref*{4category_singularities} \linebreak
\noindent\hyperlink{other_features}{Other features}\dotfill \pageref*{other_features} \linebreak
\noindent\hyperlink{invertibility}{Invertibility}\dotfill \pageref*{invertibility} \linebreak
\noindent\hyperlink{popup_labels}{Popup labels}\dotfill \pageref*{popup_labels} \linebreak
\noindent\hyperlink{theorems}{Theorems}\dotfill \pageref*{theorems} \linebreak
\noindent\hyperlink{coordinates}{Coordinates}\dotfill \pageref*{coordinates} \linebreak
\noindent\hyperlink{related_entries}{Related entries}\dotfill \pageref*{related_entries} \linebreak
\noindent\hyperlink{References}{References}\dotfill \pageref*{References} \linebreak


\hypertarget{introduction}{}\subsection*{{Introduction}}\label{introduction}

\hypertarget{overview}{}\subsubsection*{{Overview}}\label{overview}

\emph{Globular} is a web-based [[proof assistant]] for finitely-presented [[semistrict]] [[globular set|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:

\begin{itemize}%
\item \href{http://globular.science}{http://globular.science}

\end{itemize}
\textbf{We recommend the Chrome browser.}

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

\begin{itemize}%
\item Monoidal 3-category
\item Monoidal 2-category, optionally with a braiding
\item Monoidal category, optionally with a braiding or symmetry

\end{itemize}
The model of [[semistrict]] higher categories that \emph{Globular} uses puts all the weak structure in the interchangers, and higher associated structures. At the level of [[3-categories]], \emph{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.

\emph{Globular} is free to use, and \href{https://github.com/jamievicary/globular}{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 \href{http://www.cs.ox.ac.uk/people/jamie.vicary/}{Jamie Vicary}. \emph{Globular} has been developed in the \href{http://www.cs.ox.ac.uk/activities/quantum/}{Quantum Group} of the \href{http://www.cs.ox.ac.uk/}{Department of Computer Science} at the \href{http://www.ox.ac.uk/}{University of Oxford}, by \href{https://www.cs.ox.ac.uk/people/krzysztof.bar/}{Krzysztof Bar}, Katherine Casey, \href{http://www.cs.ru.nl/A.Kissinger/}{Aleks Kissinger}, \href{http://www.cs.ox.ac.uk/people/jamie.vicary/}{Jamie Vicary} and \href{}{Caspar Wylie}.

If you've never used  before, the \href{https://youtu.be/QXZJvXgs0xk}{tutorial video} is a good place to start. To report a bug, please use the \href{https://github.com/jamievicary/globular/issues}{issue tracker}.

We are extremely grateful to John Baez, Manuel B\"a{}renz, Bruce Bartlett, Eugenia Cheng, Chris Douglas, Eric Finster, Nick Gurski, Andr\'e{} Henriques, Samuel Mimram and Dominic Verdon for useful discussions.

Globular will soon followed by a successor tool \emph{[[homotopy.io]]}.

 If you would like to cite \emph{Globular}, you can use the BiBTeX entry

\begin{verbatim}  @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}}\end{verbatim}
\hypertarget{example_proofs}{}\subsubsection*{{Example proofs}}\label{example_proofs}

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

\begin{itemize}%
\item \textbf{Frobenius implies associative} (\href{http://globular.science/1512.004}{globular.science/1512.004}). In a monoidal category, if multiplication and comultiplication morphisms are unital, counital and Frobenius, then they are associative and coassociative.
\item \textbf{Strengthening an equivalence} (\href{http://globular.science/1512.007}{globular.science/1512.007}). In a 2-category, an equivalence gives rise to an adjoint equivalence, satisfying the snake equations.
\item \textbf{Pentagon and triangle implies $\lambda_I = \rho_I$} (\href{http://globular.science/1512.002}{globular.science/1512.002}). In a monoidal 2-category, if a pseudomonoid object satisfies pentagon and triangle equations, then it satisfies $\lambda_I = \rho_I$.
\item \textbf{The antipode is an algebra homomorphism} (\href{http://globular.science/1512.011}{globular.science/1512.011}). For a Hopf algebra structure in a braided monoidal category, the antipode is an algebra anti-homomorphism. (Thanks to \href{https://www.cs.ox.ac.uk/people/dominic.verdon/}{Dominic Verdon} for formalizing this.)
\item \textbf{The Perko knots are isotopic} (\href{http://globular.science/1512.012}{globular.science/1512.012}). The \href{http://mathforum.org/mathimages/index.php/Perko_pair_knots}{Perko knots} are a pair of 10-crossing knots stated by Little in 1899 to be distinct, but proven by Perko in 1974 to be isotopic. Here we give the isotopy proof. A nice feature is that the second and third Reidemeister moves do not have to be entered, since they are already implied by the 3-category axioms.
\item \textbf{The pants bordism is commutative} (\href{http://globular.science/1601.005}{globular.science/1601.005}). For an oriented dualizable object in a monoidal 2-category, the associated pants bordism is commutative. (Based on unpublished notes by \href{http://www.southalabama.edu/mathstat/personal_pages/carter/}{Scott Carter}.)
\item \textbf{K=P\#P} (\href{http://globular.science/1605.003}{globular.science/1605.003}). As knotted spheres in 4 dimensions, the Klein bottle is isotopic to the connect sum of two cross caps. (Based on the movie move proof in Section 2.3 of \href{https://books.google.ca/books/about/Knotted_Surfaces_and_Their_Diagrams.html?id=zN7xBwAAQBAJ&redir_esc=y}{\emph{Knotted Surfaces and their Diagrams}} by Scott Carter and Masahico Saito.)
\item \textbf{The 1-twist spun trefoil is unknotted.} (\href{http://globular.science/1607.003}{globular.science/1607.003}). For every classical (1,1)-knot, the knotted surface in $\mathbb{R}^4$ given by its 1-twist spin is unknotted. Here we give the explicit unknotting isotopy for the trefoil. (Based on the movie move proof in Carter and Saito. Formalization by Scott Carter.)
\item \textbf{Swallowtail coherence} (\href{http://globular.science/1512.006}{globular.science/1512.006}). In a 3-category, an adjunction of 1-morphisms gives rise to a coherent adjunction satisfying the swallowtail equations.
\item \textbf{Butterfly coherence} (\href{http://globular.science/1605.002}{globular.science/1605.002}). In a 4-category, an adjunction of 1-morphisms gives rise to a coherent adjunction satisfying the butterfly equations. (Developed by Krzysztof Bar and Jamie Vicary.)
\item \textbf{Kirby calculus and 4-manifolds} (\href{http://globular.science/1808.001}{globular.science/1808.001}). It's well-known that the braid groups are 3-endomorphism spaces in the free 3-category over a single object and a single (nontrivial) 2-morphism. In Kirby calculus (using the ``dotted circle convention'' by Akbulut), smooth 4-manifolds are specified by links. By adding a few more generators and relations (for handle slides and handle cancellations, a.k.a. Kirby moves), Kirby diagrams are the endomorphisms of the 2-identity in the previously mentioned 3-category. Some example manifolds are defined and some example diffeomorphisms are formalised. (By Manuel Bärenz)

\end{itemize}
\hypertarget{basic_functionality}{}\subsection*{{Basic functionality}}\label{basic_functionality}

\hypertarget{overview_2}{}\subsubsection*{{Overview}}\label{overview_2}

\textbf{Signatures and diagrams.} Using \emph{Globular} involves two main techniques: building the \emph{signature}, and building a \emph{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 [[globular set|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 \emph{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 \emph{equation} $C[f]=C[g]$. In a slogan, this is \emph{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.

\textbf{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.

\textbf{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.

\textbf{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.

\hypertarget{manipulating_diagrams}{}\subsubsection*{{Manipulating diagrams}}\label{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 $D$ is $k$-dimensional.

\begin{itemize}%
\item \textbf{Creation.} If the current diagram is empty, clicking the icon of a cell in the signature constructs a diagram which consists solely of the selected generator.
\item \textbf{Rewriting.} Selecting a $(k+1)$-cell $G$ from the signature displays a list of all the ways that its source $s(G)$ can be identified as a subdiagram of $D$. Choosing element of this list will then modify $D$, deleting the part of it which was chosen as matching the source $s(G)$, and replacing it with the target $t(G)$.
\item \textbf{Attaching.} Selecting a $p$-cell $G$ for $p \leq k$ displays a list of all the ways that $G$ can be attached to $D$ along one of its boundaries. Choosing an element of this list performs the attachment.

\end{itemize}
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.

\begin{itemize}%
\item \textbf{Clear \emph{c}.} Deletes the current diagram.
\item \textbf{Identity \emph{i}.} Builds the identity $(k+1)$-diagram on the current $k$-diagram.
\item \textbf{Source \emph{s}.} Saves the current diagram as the source of a new generator.
\item \textbf{Target \emph{t}.} Saves the current diagram as the target of a new generator.
\item \textbf{Restrict \emph{r}.} Replaces the current diagram with the subdiagram currently being viewed (see \hyperlink{changingtheview}{Changing the view}.)
\item \textbf{Theorem \emph{h}.} Creates a new theorem witnessing the current diagram (see \hyperlink{invertibility}{Invertibility}.)
\item \textbf{Graphic \emph{g}.} Downloads a PNG representation of the current diagram.

\end{itemize}
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.

\begin{itemize}%
\item \textbf{Click.} This attempts to attach or rewrite, as appropriate for the location of the click, with an element of the signature. If an element of the signature is marked as invertible, then the higher structure this implies will also be considered for attachment.
\item \textbf{Click-and-drag.} This attempts to attach or rewrite using an interchanger, or naturality for the interchanger, or invertibility of some cell. This is sensitive to both the click location and the direction of the drag, in a way which should be intuitive. This also allows cells to be cancelled from the top or bottom of a diagram.

\end{itemize}
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, \emph{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 \emph{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!

\hypertarget{changingtheview}{}\subsubsection*{{Changing the view}}\label{changingtheview}

\emph{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 \emph{projection} and \emph{slicing}, controlled by number scrollers which appear in the top-right of a diagram.

\begin{itemize}%
\item \textbf{Project.} This determines the number of dimensions to be projected; it can take any value $p$ in the range $0 \leq p \leq k$. Projecting a dimension causes it to be effectively ignored by \emph{Globular}; it is as if you are looking at a shadow of the true image. The resulting diagrams are exactly the \emph{singularity graphics} which are a common tool in [[Morse theory|higher Morse theory]].
\item \textbf{Slice.} Having decided to project out $p$ dimensions, and supposing the image being displayed is $v$-dimensional (for $v \in \{0,1,2\}$), that leaves $k - p - v$ dimensions still to be handled. If this sum is positive, coordinates must be chosen using the slice controls to position the view within an appropriate $v$-dimensional subdiagram.

\end{itemize}
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.)

\hypertarget{technical_implementation_details}{}\subsubsection*{{Technical implementation details}}\label{technical_implementation_details}

 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.

\hypertarget{singularities}{}\subsection*{{Singularities}}\label{singularities}

\hypertarget{overview_3}{}\subsubsection*{{Overview}}\label{overview_3}

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 \emph{Globular}, composition works differently: a $p$-cell and a $q$-cell can be composed in just \emph{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 \emph{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 \emph{Globular} \emph{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 \emph{resolves} the singularity that would be created if this composite were actually formed. These singularity resolutions manifest in \emph{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 \emph{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.

\hypertarget{2category_singularities}{}\subsubsection*{{2-category singularities}}\label{2category_singularities}

\textbf{Interchangers}

\begin{itemize}%
\item \emph{Composite:} two $2$-cells composed along a common boundary 0-cell, forming a 3-cell resolution.
\item \emph{Interface:} When unprojected, click the vertex to be interchanged and drag it up or down; if the interchanger is ambiguous because the source or target is the identity, then make your drag slightly to the left or right. When projected, grab the wire to be interchanged, and drag in the desired direction.

\end{itemize}
 $\mathraisebox{1.8cm}{\to}$  $\qquad\qquad$ 

\hypertarget{3category_singularities}{}\subsubsection*{{3-category singularities}}\label{3category_singularities}

\textbf{Naturality of the interchanger in one variable}

\begin{itemize}%
\item \emph{Composite:} a $2$-cell and a $3$-cell composed along a common boundary 0-cell, forming a 4-cell resolution.
\item \emph{Interface:} \ldots{}

\end{itemize}
\hypertarget{4category_singularities}{}\subsubsection*{{4-category singularities}}\label{4category_singularities}

\textbf{Naturality of naturality of the interchanger in one variable}

\begin{itemize}%
\item \emph{Composite:} a 2-cell and a 4-cell composed along a common boundary 0-cell, forming a 5-cell resolution.
\item \emph{Interface:} \ldots{}

\end{itemize}
\textbf{Naturality of the interchanger in two variables}

\begin{itemize}%
\item \emph{Composite:} two 3-cells composed along a common boundary 0-cell, forming a 5-cell resolution.
\item \emph{Interface:} \ldots{}

\end{itemize}
\textbf{Naturality of invertibility of the interchanger}

\begin{itemize}%
\item \emph{Composite:} \ldots{}
\item \emph{Interface:} \ldots{}

\end{itemize}
\textbf{Contractible 3rd Reidemeisterators}

\begin{itemize}%
\item \emph{Composite:} \ldots{}
\item \emph{Interface:} \ldots{}

\end{itemize}
\hypertarget{other_features}{}\subsection*{{Other features}}\label{other_features}

\hypertarget{invertibility}{}\subsubsection*{{Invertibility}}\label{invertibility}

A $k$-cell $f:A \to B$ in an $\infty$-category is \emph{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 \emph{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.

\hypertarget{popup_labels}{}\subsubsection*{{Popup labels}}\label{popup_labels}

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  isn't really aware that the lines curve, so you will need to take care when clicking or clicking-and-dragging that  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.

\begin{itemize}%
\item `X inverse' describes the $k$-cell which is the inverse of $X$
\item `X, insert' describes the canonical $(k+1)$-cell of type $\text{id} _{s(X)} \to X . X^{-1}$
\item `X, cancel' describes the canonical $(k+1)$-cell of type $X . X^{-1} \to \text{id} _{s(X)}$
\item `Interchanger' describes the height-exchange cell
\item `Pull-through interchanger above', `Pull-through interchanger underneath', `Pull-through inverse interchanger above' and `Pull-through inverse interchanger underneath' describe the 4 different ways that a cell can be pulled through an interchanger

\end{itemize}
Note that interchangers are of dimension at least 3, and pull-throughs are of dimension at least 4.

\hypertarget{theorems}{}\subsubsection*{{Theorems}}\label{theorems}

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:

\begin{itemize}%
\item A $k$-generator $T$ with source $s(D)$ and target $t(D)$
\item An invertible $(k+1)$-generator $P$ with source $T$ and with target $D$

\end{itemize}
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.

\hypertarget{coordinates}{}\subsubsection*{{Coordinates}}\label{coordinates}

Composites produced by  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.

\hypertarget{related_entries}{}\subsection*{{Related entries}}\label{related_entries}

[[!include proof assistants and formalization projects -- list]]

\hypertarget{References}{}\subsection*{{References}}\label{References}

\begin{itemize}%
\item Krzysztof Bar, [[Aleks Kissinger]], [[Jamie Vicary]], \emph{Globular: an online proof assistant for higher-dimensional rewriting}, \href{https://arxiv.org/abs/1612.01093}{arXiv:1612.01093}


\item [[Jamie Vicary]], \emph{Globular tutorial video}, 2015-12-07 \href{https://youtu.be/QXZJvXgs0xk}{15 minute video}


\item [[Jamie Vicary]], \emph{Data Structures for Quasistrict Higher Categories}, referencing \href{https://arxiv.org/abs/1610.06908}{arxiv:1610098}, 2016-12-05 talk at Simons Institute \href{https://youtu.be/9w8t0Ze08l4}{48 minute video}



\end{itemize}


\end{document}