A Type-Theoretical Definition of Weak {\omega}-Categories

TL;DR

This paper develops a dependent type theory that models weak {}-categories, generalizing previous definitions and providing a formal, canonical framework with an implemented proof system.

Contribution

It introduces a type-theoretical framework for weak {}-categories based on globular presheaves and coherators, with a canonical characterization of pasting schemes and an implementation.

Findings

Provides a formal type-theoretical model of weak {}-categories.

Defines pasting schemes as derivable contexts within the type theory.

Includes an implemented proof system for the proposed framework.

Abstract

We introduce a dependent type theory whose models are weak {\omega}-categories, generalizing Brunerie's definition of {\omega}-groupoids. Our type theory is based on the definition of {\omega}-categories given by Maltsiniotis, himself inspired by Grothendieck's approach to the definition of {\omega}-groupoids. In this setup, {\omega}-categories are defined as presheaves preserving globular colimits over a certain category, called a coherator. The coherator encodes all operations required to be present in an {\omega}-category: both the compositions of pasting schemes as well as their coherences. Our main contribution is to provide a canonical type-theoretical characterization of pasting schemes as contexts which can be derived from inference rules. Finally, we present an implementation of a corresponding proof system.

Equations

$$s_n\circ s_{n+1}=s_n\circ t_{n+1}\text{and}{t}_n\circ s_{n+1}=t_n\circ t_{n+1}$$

$$\begin{array}[]{c@{\hspace{3ex}}c@{\hspace{3ex}}c@{\hspace{3ex}}c}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 7.25763pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr\crcr}}}\ignorespaces{\hbox{\kern-7.25763pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{x_{0}}$}}}}}}}\ignorespaces}}}}\ignorespaces\hfil\hskip 12.91663pt&\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 7.25763pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\crcr}}}\ignorespaces{\hbox{\kern-7.25763pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{x_{0}^{-}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 13.2573pt\raise 5.15138pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8625pt\hbox{$\scriptstyle{x_{1}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 31.25763pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 31.25763pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{x_{0}^{+}}$}}}}}}}\ignorespaces}}}}\ignorespaces\hfil\hskip 12.91663pt&\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 7.25763pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\crcr}}}\ignorespaces{\hbox{\kern-7.25763pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{x_{0}^{-}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}}\ignorespaces\ignorespaces{\hbox{\kern 13.2573pt\raise 11.73471pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.44583pt\hbox{$\scriptstyle{x_{1}^{+}}$}}}\kern 3.0pt}}}}}}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern 31.25607pt\raise 3.67088pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}}\ignorespaces\ignorespaces{\hbox{\kern 13.2573pt\raise-11.58194pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.29306pt\hbox{$\scriptstyle{x_{1}^{-}}$}}}\kern 3.0pt}}}}}}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern 31.25607pt\raise-3.67088pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces{\hbox{\kern 11.11806pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{\phantom{x_{2}}\Downarrow x_{2}}$}}}}}\ignorespaces{}{\hbox{\kern 31.25763pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{x_{0}^{+}}$}}}}}}}\ignorespaces}}}}\ignorespaces\hfil\hskip 12.91663pt&\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 7.25763pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\crcr}}}\ignorespaces{\hbox{\kern-7.25763pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{x_{0}^{-}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}}\ignorespaces\ignorespaces{\hbox{\kern 13.2573pt\raise 11.73471pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.44583pt\hbox{$\scriptstyle{x_{1}^{+}}$}}}\kern 3.0pt}}}}}}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern 31.25607pt\raise 3.67088pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}}\ignorespaces\ignorespaces{\hbox{\kern 13.2573pt\raise-11.58194pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.29306pt\hbox{$\scriptstyle{x_{1}^{-}}$}}}\kern 3.0pt}}}}}}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern 31.25607pt\raise-3.67088pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces{\hbox{\kern 11.47984pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{\Downarrow\Rrightarrow\Downarrow}$}}}}}\ignorespaces{}{\hbox{\kern 31.25763pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{x_{0}^{+}}$}}}}}}}\ignorespaces}}}}\ignorespaces\\ D_{0}\hfil\hskip 12.91663pt&D_{1}\hfil\hskip 12.91663pt&D_{2}\hfil\hskip 12.91663pt&D_{3}\end{array}$$

$$\sigma =⟨t_1,\dots ,t_n⟩$$

$$\star \text{or}t\underset{A}{\to }u$$

$$\Gamma =x_1:A_1,\dots ,x_n:A_n$$

$$\dim (\star )=0\text{and}\dim (t\underset{A}{\to }u)=\dim (A)+1$$

$$\mathrm{FV}(x)=\{x\}$$

$$\mathrm{FV}(⟨⟩)=\varnothing \mathrm{FV}(⟨\sigma ,t⟩)=\mathrm{FV}(\sigma )\cup \mathrm{FV}(t)$$

$$\mathrm{FV}(\star )=\varnothing \mathrm{FV}(t\underset{A}{\to }u)=\mathrm{FV}(A)\cup \mathrm{FV}(t)\cup \mathrm{FV}(u)$$

$$\mathrm{FV}(\varnothing )=\varnothing \mathrm{FV}(\Gamma ,x:A)=\mathrm{FV}(\Gamma )\cup \{x\}\cup \mathrm{FV}(A)$$

$$\begin{gathered} \text{inferrule}\Gamma ⊢\Gamma ⊢\star \text{inferrule}\Gamma ⊢t:A \\ \Gamma ⊢u:A\Gamma ⊢t\underset{A}{\to }u \end{gathered}$$

$$\text{inferrule}\Gamma ,x:A⊢\Gamma ,x:A⊢x:A\text{inferrule}\Gamma ⊢t:B\Gamma ,x:A⊢t:B$$

$$\text{inferrule}\varnothing ⊢\text{inferrule}\Gamma ⊢A\Gamma ,x:A⊢$$

$$\begin{gathered} \text{inferrule}\Gamma ⊢⟨⟩:\varnothing \text{inferrule}\Delta ⊢\sigma :\Gamma \\ \Gamma ⊢A \\ \Delta ⊢t:A[\sigma /\Gamma ]\Delta ⊢⟨\sigma ,t⟩:(\Gamma ,x:A) \end{gathered}$$

$$\star [\sigma /\Gamma ]=\star (t\underset{A}{\to }u)[\sigma /\Gamma ]=t[\sigma /\Gamma ]\underset{A[\sigma /\Gamma ]}{\to }u[\sigma /\Gamma ]$$

$$x_i[\sigma /\Gamma ]=t_i$$

$$\begin{gathered} \text{inferrule}\Delta ⊢\sigma :\Gamma \\ \Gamma ⊢t:A\Delta ⊢t[\sigma /\Gamma ]:A[\sigma /\Gamma ] \end{gathered}$$

$$\sigma \circ \tau =⟨t_1[\tau ],\dots ,t_n[\tau ]⟩$$

$${\text{id}}_{\Gamma }=⟨x_1,\dots ,x_n⟩$$

$$\begin{gathered} \text{inferrule}{\rm Y}⊢\tau :\Delta \\ \Delta ⊢\sigma :\Gamma {\rm Y}⊢\sigma \circ \tau :\Gamma \text{inferrule}\Gamma ⊢\Gamma ⊢{\text{id}}_{\Gamma }:\Gamma \end{gathered}$$

$$x:\star ,y:\star ,z:\star ,f:x\underset{\star }{\to }y,g:x\underset{\star }{\to }y,h:z\underset{\star }{\to }y,\alpha :f\underset{x\underset{\star }{\to }y}{\to }g$$

$$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 5.85764pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\crcr}}}\ignorespaces{\hbox{\kern-5.85764pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{x\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 12.65393pt\raise 6.1111pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{f}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 29.85764pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 29.85764pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{y}$}}}}}}}\ignorespaces}}}}\ignorespaces\qquad\to\qquad\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 5.54515pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr\crcr}}}\ignorespaces{\hbox{\kern-5.54515pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{z\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{}{{}{{}{{}{{}{{}}{}{{}{{}}{}{{}{{}{{}{{}{{}}{}{{}}}}}}}}}}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{}{{}{{}}}\ignorespaces\ignorespaces{\hbox{\kern 19.0919pt\raise 0.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8264pt\hbox{$\scriptstyle{g}$}}}\kern 3.0pt}}}}}}\ignorespaces{}{}{}{}{{}{{}}{}{{}}{}{{}}{}{{}}{}{{}{{}}{}{{}{{}{{}{{}}{}{{}}{}{{}}}}}}}{\hbox{\kern 3.2935pt\raise-2.99599pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}{}}{}}}}\ignorespaces{}\ignorespaces}}}}\ignorespaces$$

$$T:{\mathcal{C}}^{\text{op}}\to \mathbf{Fam}$$

$$TA=({\mathrm{Tm}}_A^{\Gamma }{)}_{A\in {\mathrm{Ty}}^{\Gamma }}$$

$$x_0\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$x\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$x\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$x\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$D_2$$

$$D_{i_0}$$

Full text

I Introduction

I-A Weak $\omega$-categories

In a strict $\omega$-category, the axioms are designed to ensure that the composite of any collection of composable cells is uniquely defined. Whichever way we choose to compute this composite will always give rise to the same result. For instance, if we consider the situation where we have three sequentially composable cells, this forces composition to be associative. In a weak $\omega$-category, our goal is to achieve a similar uniqueness, but without resorting to equality: two compositions of $n$-cells should be related by an $(n+1)$-cell (which should be unique up to $(n+2)$-cells, etc.). We now have coherence cells, which themselves should have coherence cells, etc.

Achieving a reasonable definition of weak $\omega$-categories is not an easy task. Many proposals now exist, each with its own geometric flavor and collection of techniques. Often these techniques pass through sophisticated categorical machinery, and making practical use of the definition can be challenging. In this paper, we take up the definition proposed by Grothendieck [9] for $\omega$-groupoids (categories in which every cell is invertible), and later simplified and extended to a definition of $\omega$-categories by Maltsiniotis [13]. This definition was studied in detail in Ara’s thesis [2] (who showed that it is equivalent to Batanin’s definition using contractible operads [3]). The first difficulty overcome by this proposal is the definition of what it means for a collection of cells to be “composable” via the introduction of what we will refer to as pasting schemes in what follows. From here, the definition mainly consists in formally iteratively adding composites for such pasting schemes while preserving previously defined compositions (although there are, of course, some subtleties here). Note that contrary to the usual, explicit definitions of low-dimensional weak $n$-categories (e.g. bicategories or tricategories) which insist on having compositions generated by binary and nullary (identity) compositions, this definition is “unbiased” in the sense that compositions of all reasonable shapes are taken as primitive operations.

I-B A type-theoretical definition

The goal of this article is to reformulate this definition in type-theoretic terms, which is to say to present a type theory such that the (set-theoretic) models of the theory should be precisely weak $\omega$-categories. The idea of formulating $1$-categories in type theory dates back to Cartmell [6]. More recently, in his thesis [5], Brunerie has introduced a type-theoretical definition of weak $\omega$-groupoids, with the aim of showing that types in homotopy type theory possess such a structure (see also [11, 17, 1] for other work in this direction). In this article, we generalize and extend his work in order to give a definition for $\omega$-categories. The main contribution here is to characterize pasting schemes in type theory, a step which is not required for defining $\omega$-groupoids.

There are a number of reasons why one might seek such a reformulation. First, it provides us with a syntax for $\omega$-categories which can be quite convenient in practice: in particular, one can give meta-theoretic proofs by induction on the structure of terms. Second, it has didactic merits: our definition consists in only a few inference rules, and should be comprehensible to anyone with some experience in logic or type systems. That is, we keep the categorical prerequisites to a minimum. Third, it is compact lending itself to concrete computations. Finally, it is mechanizable meaning that one can give a typechecking algorithm for determining if a given term is a valid coherence in an $\omega$-category. To our knowledge there are only two such tools for checking proofs in higher categories. The first one is Opetopic [8], based on opetopic categories, coming with a very different definition and tools. The second one is Globular [18], based on the theory of semi-strict categories. While this theory allows for much shorter proofs and has a very nice graphical interface for constructing them, a complete set of axioms which should be satisfied in high-dimensions is not known yet (not even whether there is a reasonable such set of axioms); on the other hand, our tool is based on a firm theory, but requires significantly more small-step manipulations in the proofs.

I-C Plan of the paper

We begin by introducing a type-theoretical definition of globular sets (Section II), then characterize and study pasting schemes among them (Section III) and use those to define weak $\omega$-categories (Section IV). We finally briefly present an implementation (Section V) and conclude (Section VI).

The authors would like to thank Dimitri Ara for his helpful discussions on the topic of this paper. This work was supported by the CATHRE ANR grant ANR-13-BS02-0005-02.

II A type theory for globular sets

Before proceeding to the complete definition of $\omega$-categories, we introduce first in this section a type theory whose models are precisely globular sets, see also [11, 17]. This simpler theory contains only the context and type formation rules, but we present it here and study it in detail in order to make our work easier when considering the complete system in Section IV.

II-A Globular sets

The definition of $\omega$-categories which concerns us here is based on the notion of globular set. A globular set may be seen as an higher-dimensional generalization of a (directed) graph, consisting not only of edges, but of edges between edges and so on.

Definition 1**.**

A globular set $G$ consists of a family $(G_{n})_{n\in\mathbb{N}}$ of sets together with two families of maps $s_{n},t_{n}:G_{n+1}\to G_{n}$ indexed by $n\in\mathbb{N}$ such that

[TABLE]

for every $n\in\mathbb{N}$. A morphism $f:G\to G^{\prime}$ between globular sets $G$ and $G^{\prime}$ consists of a family of functions $f_{n}:G_{n}\to G^{\prime}_{n}$ such that $s_{n}\circ f_{n+1}=f_{n}\circ s_{n}$ and $t_{n}\circ f_{n+1}=f_{n}\circ t_{n}$ for every $n\in\mathbb{N}$. We write $\mathbf{GSet}$ for the resulting category.

In a globular set $G$, the elements of $G_{n}$ are called $n$-cells (cells whose dimension is $n$) and the functions $s_{n}$ and $t_{n}$ respectively associate to an $(n+1)$-cell its source and target $n$-cell. We say that a cell is top-dimensional when it is neither the source nor the target of another cell. We sometimes write $s^{m}_{n}=s_{n}\circ s_{n+1}\circ\ldots\circ s_{m-1}$ for the iterated source function. The iterated target function, $t^{m}_{n}$, is defined similarly.

The set of all cells of a globular set $G$ is denoted $G_{\infty}=\coprod_{n\in\mathbb{N}}G_{n}$ and the cardinal of $G$ is that of $G_{\infty}$. We say that $G$ is finite when $G_{\infty}$ is finite, or equivalently when $G_{n}$ is finite for any $n\in\mathbb{N}$ and there is $N\in\mathbb{N}$ such that $G_{n}=\emptyset$ for every $n\geq N$. The full subcategory on finite globular sets is denoted $\mathbf{FinGSet}$.

Example 2*.*

The diagram

\textstyle{x\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{\phantom{\alpha}\Downarrow\alpha}$$\textstyle{y}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces z}$$\scriptstyle{h}

depicts the globular set $G$ with $G_{0}=\{x,y,z\}$, $G_{1}=\{f,g,h\}$, $G_{2}=\{\alpha\}$ and $G_{n}=\emptyset$ for $n\geq 3$, with $s_{1}(\alpha)=f$, $t_{1}(\alpha)=g$, $s_{0}(f)=x$, $t_{0}(f)=y$, etc.

Equivalently, the category $\mathbf{GSet}$ of globular sets can be defined as the category $\hat{\mathbf{G}}$ of presheaves over the category $\mathbf{G}$ whose objects are integers and morphisms are generated by $s_{n},t_{n}:n\to n+1$, for $n\in\mathbb{N}$, subject to relations which are dual of (1). As with any presheaf category, we are provided with the Yoneda embedding $Y:\mathbf{G}\to\hat{\mathbf{G}}$. Given an object $n\in\mathbf{G}$, we write $D_{n}=Yn$ and call it the $n$-disk: its set of $k$-cells is $\{x_{k}^{-},x_{k}^{+}\}$ for $k<n$, $\{x_{k}\}$ for $k=n$ and $\emptyset$ otherwise:

[TABLE]

We also write $\sigma_{n}^{m}=Ys_{n}^{m}:D_{n}\to D_{m}$ (resp. $\tau_{n}^{m}=Yt_{n}^{m}$) for the canonical inclusion of an $n$-disk as the source (resp. target) of an $m$-disk.

Equivalently, globular sets can also be defined coinductively:

Definition 3**.**

A globular set $G$ consists of a set $G$ together with, for all elements $x,y\in G$, a globular set $G_{x,y}$.

II-B Syntactic constructions

We suppose fixed an infinite countable set of variables $x,y,\ldots$. A term in the theory will always be a variable in this section. (The distinction between terms and variable will become meaningful starting from Section IV). A substitution $\sigma$ is a list

[TABLE]

of terms $t_{i}$, the empty substitution being denoted $\langle\rangle$. The types are defined inductively as being either

[TABLE]

where $A$ is a type and $t$ and $u$ are terms. A context $\Gamma$ is a list

[TABLE]

of pairs $x_{i}:A_{i}$ consisting of a variable $x_{i}$ and a type $A_{i}$, what we sometimes write $\Gamma=(x_{i}:A_{i})_{1\leq i\leq n}$, the empty context being denoted $\emptyset$.

Definition 4**.**

The dimension $\dim(A)$ of a type $A$ is the natural number defined inductively by

[TABLE]

Given a context $\Gamma=(x_{i}:A_{i})_{1\leq i\leq n}$, its dimension is $\max\{\dim(A_{i})\ |\ 1\leq i\leq n\}$.

The reader will observe that these definitions are standard for the construction of a dependent type theory. We would like, however, to emphasize the geometric intuition that this syntax naturally captures, specifically, that of a finite globular set: a variable $x$ corresponds to a cell and its type $A$ indicate its dimension (namely, $\dim(A)$) as well as its source and its target. For instance, a variable $x:\star$ corresponds to a [math]-cell and a variable $x:t\underset{A}{\to}u$ corresponds to a $(\dim(A)+1)$-cell whose source is $t$ and target is $u$.

Definition 5**.**

The set of free variables is defined

• •

on terms by

[TABLE]

• •

on substitutions by

[TABLE]

• •

on types by

[TABLE]

• •

on contexts by

[TABLE]

II-C Typing rules

As usual in dependent type theories, we consider four different kinds of judgments whose informal interpretation is the following:

• •

$\Gamma\vdash$ means $\Gamma$ is a context,

• •

$\Gamma\vdash A$ means $A$ is a type in context $\Gamma$,

• •

$\Gamma\vdash t:A$ means $t$ has type $A$ in context $\Gamma$,

• •

$\Gamma\vdash\sigma:\Delta$ means that $\sigma$ is a substitution of type $\Delta$ in context $\Gamma$.

A judgment holds when it is derivable using the following inference rules, which we call the globular type theory.

II-C1 Rules for types

[TABLE]

II-C2 Rules for terms

[TABLE]

where we suppose $x\not\in\mathop{FV}(t)\cup\mathop{FV}(B)$ in the second rule

II-C3 Rules for contexts

[TABLE]

where we suppose $x\not\in\mathop{FV}(\Gamma)$ in the second rule

II-C4 Rules for substitutions

[TABLE]

The notation for the application of substitutions $A[\sigma/\Gamma]$ is explained in next section.

Lemma 6**.**

The following can be shown.

• •

If $\Gamma\vdash t:A$ holds then $\Gamma\vdash A$ holds.

• •

If $\Delta\vdash\sigma:\Gamma$ holds then $\Gamma\vdash$ holds.

• •

If $\Gamma\vdash A$ holds then $\mathop{FV}(A)\subseteq\mathop{FV}(\Gamma)$.

• •

*If $\Gamma\vdash$ holds then $\mathop{FV}(\Gamma)=\{x_{1},\ldots,x_{n}\}$, with $\Gamma=(x_{i}:A_{i})_{1\leq i\leq n}$. *

Finally, the following lemma allows us to identify derivable judgments and their derivations.

Lemma 7**.**

A judgment can be derived in at most one way.

II-D Substitutions

Consider a context $\Gamma=x_{1}{:}A_{1},\ldots,x_{n}{:}A_{n}$ and a substitution $\sigma=\langle t_{1},\ldots,t_{m}\rangle$ such that $\Delta\vdash\sigma:\Gamma$ holds. In this case, we necessarily have $m=n$. Given a type $A$ we write $A[\sigma/\Gamma]$ for the type obtained from $A$ by replacing each variable $x_{i}$ by the term $t_{i}$; given a term $t$, the term $t[\sigma/\Gamma]$ is defined similarly. More formally, we have

[TABLE]

on types, and

[TABLE]

on terms. Application of substitutions is compatible with typing:

Lemma 8**.**

The following rule is admissible:

[TABLE]

Given another substitution $\tau$ such that $\Upsilon\vdash\tau:\Delta$ holds, we write $\sigma\circ\tau$ for the composite substitution

[TABLE]

and given a context $\Gamma=(x_{i}:A_{i})_{1\leq i\leq n}$, the associated identity substitution is

[TABLE]

Lemma 9**.**

The following rules are admissible

[TABLE]

Moreover, composition is associative and admits identities as neutral elements.

II-E The syntactic category

We are now in position to define the category generated by this type theory.

Definition 10**.**

The syntactic category $\mathcal{S}_{\textsf{glob}}$ associated to this theory is the category whose

• •

objects are contexts $\Gamma$ such that $\Gamma\vdash$ holds,

• •

morphisms $\sigma:\Delta\to\Gamma$ are substitutions such that $\Delta\vdash\sigma:\Gamma$ holds.

The following proposition shows that, in fact, contexts can be considered as a notation for finite globular sets.

Proposition 11**.**

The category $\mathcal{S}_{\textsf{glob}}$ is equivalent to the category $\mathbf{FinGSet}^{\textnormal{op}}$.

Proof.

We construct a functor $F:\mathcal{S}_{\textsf{glob}}\to\mathbf{FinGSet}^{\textnormal{op}}$ as follows. Given a context $\Gamma=(x_{i}:A_{i})_{1\leq i\leq k}$, we define $F\Gamma$ to be the globular set $G^{\Gamma}$ with $G^{\Gamma}_{n}=\{(x_{i},i)\ |\ \dim(A_{i})=n\}$ (the second component ensures that two different instances of a variable in $\Gamma$ gives rise to two distinct cells). Given an $(n+1)$-cell $(x_{i},i)$, the type of $x_{i}$ is of the form $A_{i}=y\underset{A}{\to}z$ and we define its source and target as $s_{n}(x_{i},i)=y$ and $t_{n}(x_{i},i)=z$. The fact that the globular identities (1) hold can be shown by induction on the derivation of $\Gamma\vdash$.

Suppose given a morphism $\sigma:\Delta\to\Gamma$ with $\Gamma=(x_{i}:A_{i})_{1\leq i\leq m}$ and $\Delta=(y_{i}:B_{i})_{1\leq i\leq n}$. The substitution is of the form $\sigma=\langle z_{1},\ldots,z_{m}\rangle$ and for every index $i$ with $1\leq i\leq m$ there is an index $j_{i}$ with $1\leq j_{i}\leq n$ such that $z_{i}=y_{j_{i}}$. We then define $f^{\sigma}_{\dim(A_{i})}(x_{i},i)=(y_{j_{i}},j_{i})$. In order to formally account for the case where a same variable occurs multiple times in $\Delta$, this definition should in fact be performed by induction on the derivation of $\Delta\vdash\sigma:\Gamma$, in the expected way. By a similar induction, the morphism $f^{\sigma}$ can be shown to be a morphism of globular sets.

The functor $F$ is faithful since a substitution $\sigma$ can be recovered from $f^{\sigma}$: we have $\sigma=\langle f(x_{1},1),\ldots,f(x_{n},n)\rangle$. The functor is also full since for any morphism $f$, the substitution $\sigma$ defined as previously can be shown to be such that $\Delta\vdash\sigma:\Gamma$ holds, by induction on $\Gamma\vdash$. Finally, the functor $F$ is essentially surjective: given a globular set $G$ and an enumeration $G_{\infty}=\{x_{i}\ |\ 1\leq i\leq m\}$ of all cells compatible with dimensions (i.e. a total ordering of cells such that $i\leq j$ implies $\dim(x_{i})\leq\dim(x_{j})$), $G$ is isomorphic to the image of the context $(x_{i}:A_{i})_{1\leq i\leq m}$ where $A_{i}=\star$ if $x_{i}$ is a [math]-cell, and $A_{k}=x_{i}\underset{A_{i}}{\to}x_{j}$ if $x_{k}$ is an $(n+1)$-cell with $s_{n}(x_{k})=x_{i}$ and $t_{n}(x_{k})=x_{j}$. ∎

Example 12*.*

The context corresponding to the globular set of Example 2 is

[TABLE]

Other contexts also correspond to this globular set (for instance the one obtained by permuting $x$ and $y$), but they are isomorphic to this one. The substitution corresponding to the only morphism

[TABLE]

is $z:\star,g:z\underset{\star}{\to}z\vdash\langle z,z,g\rangle:(x:\star,y:\star,f:x\underset{\star}{\to}y)$.

II-F Models

Let us briefly recall the notion of model for a dependent type theory in categories with families [7]. The category $\mathbf{Fam}$ has families of sets $(E_{x})_{x\in B}$ as objects (the set $B$ is called the base and the set $E_{x}$ the fiber over $x$) and a morphism $(E_{x})_{x\in B}\to(E^{\prime}_{x})_{x\in B^{\prime}}$ consists in functions $f:B\to B^{\prime}$ and $(g_{x}:E_{x}\to E^{\prime}_{f(x)})_{x\in B}$.

A category with families (or cwf) consists of a category $\mathcal{C}$ together with a functor

[TABLE]

Given an object $\Gamma$ of $\mathcal{C}$, we write

[TABLE]

i.e. $\operatorname{Ty}^{\Gamma}$ for the base of $T\Gamma$ and $\operatorname{Tm}^{\Gamma}_{A}$ for the fibers. Similarly, given a morphism $\sigma:\Delta\to\Gamma$ in $\mathcal{C}$, we write $\operatorname{Ty}^{\sigma}:\operatorname{Ty}^{\Gamma}\to\operatorname{Ty}^{\Delta}$ and $\operatorname{Tm}^{\sigma}_{A}:\operatorname{Tm}^{\Gamma}_{A}\to\operatorname{Tm}^{\Delta}_{\operatorname{Ty}^{\sigma}(A)}$ for the functions constituting its image. The category $\mathcal{C}$ should moreover satisfy the following axioms: it should have a terminal object $\emptyset$ and a context comprehension operation which to an object $\Gamma$ of $\mathcal{C}$ and an element $A\in\operatorname{Ty}^{\Gamma}$ associates an object $(\Gamma,A)$, a morphism $\pi:(\Gamma,A)\to\Gamma$ and an element $p\in\operatorname{Tm}^{\Delta}_{\operatorname{Ty}^{\pi}(A)}$, in a way such that for every morphism object $\Delta$, morphism $\sigma:\Delta\to\Gamma$ and element $t\in\operatorname{Tm}^{\Delta}_{\operatorname{Ty}^{\sigma}(A)}$ there is a unique morphism $\langle\sigma,t\rangle:\Delta\to(\Gamma,A)$ such that $\pi\circ\langle\sigma,t\rangle=\sigma$ and $\operatorname{Tm}^{\langle\sigma,t\rangle}_{\operatorname{Ty}^{\pi}(A)}(p)=t$. A morphism between cwfs $T:\mathcal{C}^{\textnormal{op}}\to\mathbf{Fam}$ and $T^{\prime}:\mathcal{C}^{\prime\textnormal{op}}\to\mathbf{Fam}$ consists of a functor $F:\mathcal{C}^{\textnormal{op}}\to\mathcal{C}^{\prime\textnormal{op}}$ and a natural transformation $\phi:T\to T^{\prime}\circ F$, preserving the terminal object and context comprehension on the nose. Given two morphisms $(F_{1},\phi_{1}):T\to T^{\prime}$ and $(F_{2},\phi_{2}):T\to T$, a 2-morphism $\theta:(F_{1},\phi_{1})\Rightarrow(F_{2},\phi_{2})$ is a natural transformation $\theta:F_{1}\to F_{2}$ such that $T\theta\circ\phi_{1}=\phi_{2}$.

Typically, the syntactic category $\mathcal{S}_{\textsf{glob}}$ is canonically a cwf when equipped with the functor $T:\mathcal{S}_{\textsf{glob}}^{\textnormal{op}}\to\mathbf{Fam}$ such that for a context $\Gamma$, we have $\operatorname{Ty}^{\Gamma}$ the set of types $A$ such that $\Gamma\vdash A$ and $\operatorname{Tm}^{\Gamma}_{A}$ the set of terms $t$ such that $\Gamma\vdash t:A$ (thus the notations above). The category $\mathbf{Set}$ is also canonically a cwf with the functor which to a set $X$ associates the family with $\operatorname{Ty}^{X}$ being the collection of functions $f:Y\to X$ with $X$ as codomain and $\operatorname{Tm}^{X}_{f}$ being the set of sections of $f$.

A model of the globular type theory is a morphism of cwfs $\mathcal{S}_{\textsf{glob}}\to\mathcal{C}$ for some cwf $\mathcal{C}$. A set-theoretic model is a model where $\mathcal{C}=\mathbf{Set}$.

Proposition 13**.**

The category of set-theoretic models of $\mathcal{S}_{\textsf{glob}}$ is equivalent to the category $\mathbf{GSet}^{\textnormal{op}}$.

III Pasting schemes

The main contribution of this article is to provide a simple description of pasting schemes, encoding a collection of composable cells. For instance, in a $1$-category, we expect the diagram

[TABLE]

to give rise to a unique composite (it does not depend on the order in which the morphisms are pairwise composed), but diagrams such as

[TABLE]

are not expected to be composed. A formal description of these pasting schemes in higher dimensions is not easy. It was achieved, in the globular setting, by Grothendieck [9] using abstract categorical techniques and studied combinatorially by Batanin [3].

Example 14*.*

The following diagram is a pasting scheme in a $2$- (or higher-) category:

[TABLE]

The pasting scheme above corresponds to a globular set, which can be obtained as the following colimit of disks, where the dotted arrows correspond to the obvious monomorphisms of globular sets:

[TABLE]

that is, to the colimit of the diagram

[TABLE]

of globular sets. The idea of Grothendieck’s definition [9] is that pasting schemes are precisely diagrams which can be obtained by such colimits, which are called globular sums. Our presentation given below is largely inspired of the work of Maltsiniotis [13] and Ara [2].

III-A Globular extensions

A globular category consists of a category $\mathcal{C}$ together with a functor $\mathbf{G}\to\mathcal{C}$, i.e. it is a category equipped a notion of “disk”: we write $D_{n}$ for the image of $n$ and denote in the same way the morphisms in $\mathbf{G}$ and their image. A morphism $f$ of $\mathcal{C}$ is globular when it is the image of one in $\mathbf{G}$. A globular sum is the colimit of a diagram of the form

[TABLE]

in $\mathcal{C}$, with $k\geq 0$ (the diagram cannot be empty). A globular category $\mathbf{G}\to\mathcal{C}$ is a globular extension when all globular sums exist. The category $\mathbf{GExt}$ of globular extensions is the subcategory of the slice category $\mathbf{G}/\mathbf{Cat}$ whose objects are globular extensions and morphisms are functors preserving globular sums.

By definition, there is a forgetful functor $\mathbf{GExt}\to\mathbf{G}/\mathbf{Cat}$, sending a globular extension to the underlying globular category, which admits a left (2-)adjoint. In particular, there is a free globular extension on the globular category given by the identity functor $\mathbf{G}\to\mathbf{G}$: this category is called $\mathbf{\Theta}_{0}$ (and we have a functor $\mathbf{G}\to\mathbf{\Theta}_{0}$). Alternatively, it can be characterized as follows:

Definition 15**.**

The globular extension $\mathbf{G}\to\mathbf{\Theta}_{0}$ is the one such that for every globular extension $\mathbf{G}\to\mathcal{C}$ there exists a morphism of globular extensions $\mathbf{\Theta}_{0}\to\mathcal{C}$, which is unique up to isomorphism.

Intuitively, the category $\mathbf{\Theta}_{0}$ is the category obtained by considering formal disks and freely completing it under globular sums. Its objects thus correspond to pasting schemes, but we restrict this terminology to the alternative description of those objects as globular sets, given in next section.

III-B Pasting schemes

We now recall the more usual description of pasting schemes. As for any presheaf category (see [12]) the category of globular sets $\mathbf{GSet}=\hat{\mathbf{G}}$ is the free cocompletion of the category $\mathbf{G}$, meaning that it is cocomplete and that for any functor $F:\mathbf{G}\to\mathcal{C}$, where $\mathcal{C}$ is a cocomplete category, there exists a unique (up to isomorphism) functor $\hat{F}:\hat{\mathbf{G}}\to\mathcal{C}$ which preserves colimits and makes the diagram

[TABLE]

commute, where $Y:\mathbf{G}\to\hat{\mathbf{G}}$ is the Yoneda embedding. Note that this functor makes $\hat{\mathbf{G}}$ into a globular category. Since the category $\mathbf{\Theta}_{0}$ is only required to have globular sums (and not all colimits), we can expect to recover $\mathbf{\Theta}_{0}$ as a full subcategory of $\hat{\mathbf{G}}$ consisting of globular sums of representables:

Proposition 16** ([2, Proposition 2.2.1]).**

The category $\mathbf{\Theta}_{0}$ is the full subcategory of $\mathbf{GSet}$ whose objects are globular sums of representables.

The globular sets which are the objects of $\mathbf{\Theta}_{0}$, as described by the above proposition, are called pasting schemes.

Example 17*.*

The globular set $G$ corresponding to Example 14 is the globular set with

[TABLE]

and $G_{n}=\emptyset$ for $n\geq 3$, with source and targets as indicated on the figure.

Finally, we recall how the source and target of a pasting scheme can be described, see [13] for details.

Definition 18**.**

Suppose given a pasting scheme $G$, which can be obtained as a globular sum of the form (2). Given an integer $n\in\mathbb{N}$, its $n$-boundary $\partial_{n}G$ is the colimit of the diagram obtained from (2) by replacing each object $D_{i_{m}}$ (resp. $D_{j_{m}}$) by $D_{\min(i_{m},n)}$ (resp. $D_{\min(j_{m},n)}$). Moreover, there are two canonical morphisms $\sigma_{i}^{G},\tau_{i}^{G}:\partial_{i}G\to G$ exhibiting $\partial_{i}G$ as the source and target of $G$ respectively.

Example 19*.*

Consider the following pasting scheme $G$:

[TABLE]

Its $1$-source and $1$-target are respectively

[TABLE]

(both are $\partial_{1}G$, and are in particular isomorphic, but the different namings make clear the respective inclusions $\sigma^{G}_{1}$ and $\tau^{G}_{1}$) and its [math]-source and [math]-target are respectively $x$ and $z$.

III-C A characterization

We now introduce a characterization of pasting schemes, which is apparently new and turns out to be very convenient to work with in the following. First, note that since pasting schemes are finite colimits of disks, which are finite globular sets, and colimits are computed pointwise, we have

Lemma 20**.**

Pasting schemes are finite globular sets, i.e. $\mathbf{\Theta}_{0}$ is a full subcategory of $\mathbf{FinGSet}$.

We now introduce a relation $\triangleleft$ which expresses when a cell is “before” another in a globular set. Similar relations have already been considered before, e.g. for pasting schemes [15].

Definition 21**.**

Given a globular set $G$, we define the relation $\triangleleft$ on its set $G_{\infty}$ of cells as the transitive closure of the relation such that for every $(n+1)$-cell $x\in G_{\infty}$ one has

[TABLE]

Example 22*.*

In the globular set of Example 14 (see Example 17), the relation is

[TABLE]

Example 23*.*

In the globular set of Example 2 (which is not a pasting scheme), the relation is

[TABLE]

(a partial order with $y$ as maximal element).

Example 24*.*

The relation on the globular set $D_{n}$ is

[TABLE]

Clearly, the relation is preserved by morphisms:

Lemma 25**.**

For every morphism $f:G\to G^{\prime}$ of globular sets and cells $x,y\in G_{\infty}$ such that $x\triangleleft y$, we have $f(x)\triangleleft f(y)$.

Theorem 26**.**

The pasting schemes are the non-empty finite globular sets $G$ which are $\triangleleft$-linear, meaning that for every cells $x,y\in G_{\infty}$,

[TABLE]

This condition is equivalent to the reflexive closure of $\triangleleft$ being a total order on the cells of $G$.

Proof.

We first show that the pasting schemes satisfy the linearity condition, by recurrence on $k\in\mathbb{N}$, the number of peaks in a diagram (2) whose colimit is the pasting scheme. We also show inductively that, if we call $G$ the colimit and $\iota_{k}:D_{i_{k}}\to G$ the canonical arrow we have that the successors wrt $\triangleleft$ of $\iota_{k}(x_{j_{k}})$ in $G$ are precisely

[TABLE]

where $x_{j_{k}}$ denotes the top-dimensional cell of $D_{j_{k}}$: intuitively, this cell has its successors unchanged after applying $\iota_{k}$, or equivalently its only successors are its iterated target faces. When the pasting scheme is a disk $D_{i_{0}}$, the $\triangleleft$-linearity condition is satisfied, see Example 24, and the canonical colimiting arrow $\iota_{0}:D_{i_{0}}\to D_{i_{0}}$ is the identity and thus satisfies (4). Otherwise, suppose given a diagram (2). Since this diagram is finite, connected and simply connected, its colimit can be computed using iterated pushouts [14]. We thus obtain a diagram of the form

[TABLE]

We thus consider the colimit $G$ of the subdiagram obtained by excluding $D_{j_{k}}$ and $D_{i_{k}}$, with colimiting cocone formed by the morphisms $\iota_{i}$. By induction hypothesis, the set $G$ is $\triangleleft$-linear and $\iota_{k-1}$ satisfies (4). The globular sum we are interested in is the pushout of $\iota_{k-1}\circ\tau^{i_{k-1}}_{j_{k}}$ and $\sigma^{i_{k}}_{j_{k}}$. Because of the order (3) of $D_{i_{k}}$, one easily shows that the effect of the pushout is to “insert” the cells

[TABLE]

of $D_{i_{k}}$ in (4) between $\iota_{k-1}(x_{j_{k}}^{+})$ and $\iota_{k-1}(x_{j_{k}-1}^{+})$, from which one concludes that the resulting globular set is $\triangleleft$-linear and (4) is satisfied.

Conversely, suppose given a $\triangleleft$-linear finite globular set $G\in\hat{\mathbf{G}}$. We write $x_{1},\ldots,x_{k}$ for the top-dimensional elements of $G$ in the order given by $\triangleleft$, i.e. $x_{1}\triangleleft\ldots\triangleleft x_{k}$. As any presheaf, $G$ can be obtained as the colimit of representables [12]:

[TABLE]

where $\operatorname{El}G$ denotes the category of elements of $G$. A careful examination of this diagram shows, by recurrence on $k$, that this colimit is the same as the one of the globular sum of the form (2), where $i_{n}$ is then dimension of the top-dimensional cell $x_{n}$ and $j_{n+1}$ is the greatest integer such that $t^{i_{n}}_{j_{n+1}}(x_{n})=s^{i_{n+1}}_{j_{n+1}}$ (such an integer necessarily exists because $x_{n}$ and $x_{n+1}$ are consecutive top-dimensional elements wrt $\triangleleft$). ∎

Example 27*.*

From Example 22 (resp. 23), one sees that the globular set of Example 14 (resp. 2) is a pasting scheme (resp. not a pasting scheme).

Example 28*.*

To illustrate the first part of the proof, in the case of the globular sum of Example 14, the linear orders obtained by iteratively computing the colimit using pushouts are

[TABLE]

This result enables one to immediately draw some interesting consequences:

Lemma 29**.**

A morphism between pasting schemes is necessarily a monomorphism and the only automorphism of a pasting scheme is the identity.

Proof.

Suppose given a morphism $f:G\to G^{\prime}$ between pasting schemes and consider two cells $x,y\in G_{n}$ such that $f_{n}(x)=f_{n}(y)$. If $x\neq y$ then, by Theorem 26, $x\triangleleft y$ or $y\triangleleft x$ and by Lemma 25 on has $f_{n}(x)\triangleleft f_{n}(y)=f_{n}(x)$, which is excluded by Theorem 26. This argument is the reason why we did not define $\triangleleft$ as a preorder, i.e. close it under reflexivity. The other property uses similar arguments. ∎

III-D Batanin trees

In order to make a connection with other works on the subject, we briefly recall here another representation of pasting schemes as trees introduced by Batanin [3]. The correspondence with pasting schemes is detailed in [4, 2], we recall it here in order to explain why the linear ordering of cells was to be expected. In this section, we consider finite planar rooted trees:

Definition 30**.**

A tree $T$ consists of a family of sets $(T_{n})_{n\in\mathbb{N}}$, whose elements are called $n$-vertices, together with a family of functions $d_{n}:T_{n+1}\to T_{n}$ and a total order on the set $p_{n}^{-1}(x)$ of children of $x$, for any vertex $x\in T_{n}$, such that $T_{0}$ is a singleton and $\coprod_{n\in\mathbb{N}}T_{n}$ is finite.

Given a vertex $x\in T_{n}$, we write

[TABLE]

for the totally ordered set $p_{n}^{-1}(x)$ extended with a new minimal element $-$ and a new maximal element $+$. A sector of $x$ consists in two consecutive elements of $q_{n}(x)$. To any tree $T$, one can associate a finite globular set $T_{*}$ whose $n$-cells are the sectors associated to its $n$-vertices. The source of a sector $(y_{1},y_{2})$ of $x\in T_{n+1}$ is the sector $(x^{\prime},x)$ of $f_{n}(x)$, where $x^{\prime}$ is the preceding element of $x$ in $q_{n}(f_{n}(x))$; targets are defined similarly.

By suitably defining the morphisms between trees (which is slightly more involved than one might expect), this operation extends to a functor from the category of trees to the category of pasting schemes, which can be shown to be an equivalence, i.e. pasting schemes can be represented as trees:

Proposition 31** ([4, 2]).**

The category $\mathbf{\Theta}_{0}$ is equivalent to the category of trees and suitable morphisms.

Example 32*.*

Consider the tree $T$ with $T_{0}=\{x^{0}_{0}\}$, $T_{1}=\{x^{1}_{0},x^{1}_{1},x^{1}_{2}\}$, $T_{2}=\{x^{2}_{0},x^{2}_{1}\}$, $p_{1}(x^{2}_{i})=x^{1}_{0}$ and $p_{0}(x^{1}_{i})=x^{0}_{0}$:

[TABLE]

We have figured the sectors in small letters. For instance, the sectors associated to $x^{1}_{0}$ are $f,f^{\prime},f^{\prime\prime}$ and the one associated to $x^{2}_{0}$ is $\alpha$. The globular set $T_{*}$ is precisely the pasting scheme of Example 14. The order on cells

[TABLE]

is precisely the list of sectors encountered if we draw a line around the tree starting from the bottom left (think of a child drawing the contour of his hand).

This “duality” between trees and pasting schemes was nicely explained by Joyal in [10] where he additionally introduces a generalization of the category $\mathbf{\Theta}_{0}$.

III-E A type-theoretic definition of pasting schemes

We have seen in Proposition 11 that contexts correspond to finite globular sets. Our aim is now to characterize those contexts which correspond to pasting schemes in a type-theoretic fashion, that is to say, using a system of inference rules. It turns out that this characterization yields canonical forms for pasting schemes: we have seen in Example 12 that multiple (isomorphic) contexts may correspond to a same pasting scheme, but our definition singles out exactly one. Our main tool is the linear order $\triangleleft$ studied in Section III-C. The reader will notice, however, that this order does not give rise to a well formed context. For instance, consider the pasting scheme on the left below, whose $\triangleleft$ relation is shown in the middle:

[TABLE]

A direct translation of this order as a “context” is shown on the right, but it is not a well-formed context since the variable $y$ has to be declared before $f$ whose type involves $y$. We will therefore use another enumeration of the cells and the associated context will in fact be

[TABLE]

Note that $y:\star,x:\star,f:x\underset{\star}{\to}y$ would be another sensible representation for the pasting scheme, but our typing rules will only accept the first one.

We add two new kinds of judgments to our type theory:

• •

$\Gamma\vdash_{\textsf{ps}}$ means $\Gamma$ is a context which is a pasting scheme,

• •

$\Gamma\vdash_{\textsf{ps}}x:A$ means $\Gamma$ is a partial pasting scheme (one which is being constructed), with $x$ as “free output”.

The rules for showing that a context is a pasting scheme are the following ones:

[TABLE]

[TABLE]

where on the bottom left we suppose $y,f\not\in\mathop{FV}(\Gamma)$. In the first line, the first rule allows one to conclude that a partial pasting scheme is in fact a pasting scheme, whereas the second one allows one to start constructing a pasting scheme with one [math]-cell. In the second line, the first rule allows one to attach a new cell to a pasting scheme, and the second rule to drop the possibility of attaching a cell to $f$. A context $\Gamma$ such that $\Gamma\vdash_{\textsf{ps}}$ holds is called a ps-context. Observe that every ps-context is of odd length.

Example 33*.*

The context corresponding to the pasting scheme

[TABLE]

is derived as follows:

[TABLE]

Graphically, it corresponds to constructing the pasting scheme in the following way

[TABLE]

Also, note that the variables occurring on the right precisely do so in the $\triangleleft$ order when read from top to bottom:

[TABLE]

Finally, in Figure 1, we have figured for each sequent $\Gamma\vdash_{\textsf{ps}}x:A$ the $\triangleleft$ relation (the height of each cell corresponding to its dimension), with the cell $x$ underlined.

Lemma 34**.**

Given a context $\Gamma$ such that $\Gamma\vdash_{\textsf{ps}}$ holds, $\Gamma\vdash$ also holds.

Lemma 35**.**

There is at most one way to show a statement of the form $\Gamma\vdash_{\textsf{ps}}$ or $\Gamma\vdash_{\textsf{ps}}x:A$.

Previous example should make it clear that there is a tight correspondence between type ps-contexts and pasting schemes as previously defined. First note that in a ps-context, there is no variable clash:

Lemma 36**.**

In a ps-context $\Gamma=(x_{i}:A_{i})_{1\leq i\leq n}$, for every variables $x_{i}$ and $x_{j}$ such that $x_{i}=x_{j}$ we have $i=j$.

For this reason, when associating a globular set $G^{\Gamma}$ to a ps-context $\Gamma=(x_{i}:A_{i})_{1\leq i\leq k}$, we can proceed in a simpler way than in the proof of Proposition 11 and define $G^{\Gamma}_{n}=\{x_{i}\ |\ \dim(x_{i})=n\}$ (no need to rename variables), which we will do in the following.

Proposition 37**.**

There is a bijection between pasting schemes $G$ which are such that the sets $G_{n}$ are disjoint subsets of the variables and ps-contexts.

Proof.

Suppose given a context such that $\Gamma\vdash_{\textsf{ps}}$ holds. We can show by induction on its proof that for every sequent $\Gamma\vdash_{\textsf{ps}}x:A$, the globular set $G^{\Gamma}$ associated to it is $\triangleleft$-linear and the cell corresponding to $x$ has its iterated targets as only greater elements wrt $\triangleleft$.

Conversely, suppose given a globular set $G$ satisfying the hypothesis, with cells $G_{\infty}=\{x_{1},\ldots,x_{k}\}$ such that $x_{1}\triangleleft\ldots\triangleleft x_{k}$. We can construct by recurrence on the length of a prefix of size $i$ (with $1\leq i\leq k$) a derivation of the form $\Gamma\vdash_{\textsf{ps}}x_{i}:A_{i}$ such that $G^{\Gamma}$ is the subcomplex of $G$ generated by $\{x_{1},\ldots,x_{i}\}$ (i.e. obtained by taking the closure under faces of this set).

Finally, the two operations can be checked to be mutually inverse. ∎

From this, we finally deduce:

Theorem 38**.**

The category $\mathbf{\Theta}_{0}$ is equivalent to the full subcategory $\mathcal{S}_{\textsf{ps}}$ of $\mathcal{S}_{\textsf{glob}}$ whose objects are pasting schemes.

Remark 39*.*

Note that, in fact, we have a tighter correspondence than an equivalence of categories since pasting schemes up to isomorphism are in bijection with ps-contexts up to $\alpha$-equivalence (as opposed to isomorphism), i.e. renaming of variables. Moreover, one can construct a variable-free presentation of the sequent calculus (using De Bruijn indices) which entirely removes the need for $\alpha$-equivalence.

III-F Boundaries

We now explain how to compute boundaries (see Definition 18) of ps-contexts. This is defined as a “meta-operation” on contexts.

Definition 40**.**

Given $i\in\mathbb{N}$, we define the $i$-source $\partial^{-}_{i}(\Gamma)$ of a context $\Gamma$ as $\partial^{-}_{i}(x:\star)=x:\star$ and $\partial^{-}_{i}(\Gamma,y:A,f:x\underset{A}{\to}y)$ as

[TABLE]

and the $i$-target by $\partial^{+}_{i}(x:\star)=x:\star$, and $\partial^{+}_{i}(\Gamma,y:A,f:x\underset{A}{\to}y)$ as

[TABLE]

where $\textnormal{drop}(\Gamma)$ is $\Gamma$ with the last element removed. By convention, we write

[TABLE]

Proposition 41**.**

Given a ps-context $\Gamma$ and $i\in\mathbb{N}$, the contexts $\partial_{i}^{-}(\Gamma)$ and $\partial_{i}^{+}(\Gamma)$ are ps-contexts. Moreover, they correspond to Definition 18, in the sense that

[TABLE]

and the canonical inclusions $G^{\partial_{i}^{-}(\Gamma)}\to G^{\Gamma}$ and $G^{\partial_{i}^{+}(\Gamma)}\to G^{\Gamma}$ are respectively $\sigma^{G}_{i}$ and $\tau^{G}_{i}$.

III-G A non-canonical definition

To further emphasize the fact that the previous characterization of ps-contexts is canonical in the sense that each pasting scheme has a unique derivation, we provide here a second type theoretical characterization of pasting schemes which lacks this property.

We now consider judgments of the form

[TABLE]

The main modification wrt the previous definition is that $\Delta$ is a context, i.e. we have a choice of multiple “free outputs”, whereas we only had one before. The rules are

[TABLE]

[TABLE]

where, in the last rule, $y$ and $f$ are fresh in $\Gamma$.

Proposition 42**.**

For every context $\Gamma$ such that $\Gamma\vdash_{\textsf{ps}}$ is derivable $G^{\Gamma}$ is a pasting scheme and conversely every pasting scheme is isomorphic to one of this form.

Proof.

In a derivation of $\Gamma\vdash_{\textsf{ps}}$, we can permute rules so that it corresponds (up to bookkeeping) to a derivation in the sense of Section III-E. ∎

The following example shows that there is however not a canonical ps-context associated to a pasting scheme with this variant.

Example 43*.*

The pasting scheme

[TABLE]

corresponds to both the contexts

[TABLE]

and

[TABLE]

for which we can derive that they are pasting schemes.

From a practical point of view, the main advantage of previous axiomatization of ps-contexts over this one is that it can be used to simply check whether a context is a pasting scheme or not, without having to provide a proof or run an complicated proof-search algorithm.

IV Weak $\omega$-categories

In this section, we finally use our characterization of pasting schemes to give a type theoretic definition of weak $\omega$-categories.

IV-A A type-theoretic definition of $\omega$-groupoids

The basic idea in order to define an $\omega$-category is that every pasting scheme should have a composition. We thus introduce a new family of terms to our syntax, called coherences, and denoted

[TABLE]

Each coherence is indexed by a context $\Gamma$, a type $A$ and a substitution $\sigma$. Such a term should be thought of as a constant $\mathsf{coh}_{\Gamma,A}$ which takes a pasting scheme $\Gamma$ and produces a value of type $A$, corresponding to its composition. The substitution $\sigma$ corresponds to formally applying a substitution to it. By convention, we write $\mathsf{coh}_{\Gamma,A}$ instead of $\mathsf{coh}_{\Gamma,A}[\langle\rangle]$ in the following, and we extend the rules for substitution (see Section II-D) by

[TABLE]

The free variables of a coherence are defined as

[TABLE]

Indeed, the coherence binds the variables of $\Gamma$ in $A$. In practice, we will always have $\mathop{FV}(A)\subseteq\mathop{FV}(\Gamma)$ and thus $\mathop{FV}(A)\setminus\mathop{FV}(\Gamma)=\emptyset$. Note that, contrary to the situation in earlier sections, the addition of coherences means that terms are no longer necessarily variables, i.e. the distinction between the two syntactic classes is relevant.

Since, in an $\omega$-category, one expects to have composites of all pasting schemes, a naive definition would simply assert their existence. For example, let us consider the consequences of the following rule:

[TABLE]

Remark 44*.*

The rule should in fact be written

[TABLE]

so that Lemma 8 still holds. Alternatively, one can add the rule of the lemma to the type theory. We will ignore this detail in what follows.

Example 45*.*

The following coherences are all derivable:

• •

Every object has an associated identity:

[TABLE]

• •

Every pair of composable morphisms have a composition:

[TABLE]

• •

There is a morphism witnessing that identities are neutral elements on the left (the left-unitor):

[TABLE]

where $\mathsf{id}_{x}$ is a notation for the first derived coherence, and $\mathsf{comp}(\mathsf{id}_{x},f)$ is a notation for the composite of $\mathsf{id}_{x}$ and $f$, defined using the second coherence. This morphism has a (weak) inverse:

[TABLE]

(this is an inverse only up to weakly invertible morphisms).

• •

Every triple of composable morphisms have a composition:

[TABLE]

• •

In fact, this system admits “partial composition” operations, ignoring some variables in the context. For instance, in a context as above, we can compose only $f$ and $g$ (and forget about $h$):

[TABLE]

• •

Every morphism admits a weak inverse:

[TABLE]

The last coherence should make it clear that the unrestricted composition rule above yields not a definition of an $\omega$-category, but of an $\omega$-groupoid. In fact, this definition is very close to Brunerie’s definition [5, Appendix A]: this is no accident since our work is largely inspired by his. The only difference between the two definitions of $\omega$-groupoid is that Brunerie uses a more liberal notion of pasting scheme, which is called a contractible context, generated by the following rules:

[TABLE]

[TABLE]

where $y,f\not\in\mathop{FV}(\Gamma)$ for the second one. As an illustration of the difference, the context

[TABLE]

is contractible but not a pasting scheme. We will see in next section that using our pasting schemes allows us to formulate a definition for $\omega$-categories.

IV-B Type-theoretic definition of $\omega$-categories

In order to characterize $\omega$-categories, we will need to restrict the rule of the previous section in such a way that inverses are excluded, but such that all reasonable structural operations remain. In fact, the rule (5) will be replaced by two separate rules. Indeed, the “problem” with derivation of inverses (last point of Example 45) is that it exchanges source and target, so we add a side condition ensuring that this does not happen:

[TABLE]

whenever

[TABLE]

This rule allows one to derive all the “operations” required in an $\omega$-category (e.g. composition and identities), but not their coherences (for instance, the witnesses for identity being a neutral element shown in previous section are not derivable). We therefore add another rule to compensate:

[TABLE]

whenever

[TABLE]

The side condition forbids “partial compositions”, which would allow for too many invertible operations otherwise (see previous section). With these two rules, we can derive the operations required to be present in an $\omega$-category and only those. For instance, all the coherences of Example 45 can be derived excepting the last one. Some more practical illustrations are given in Section V.

Writing $\mathcal{S}_{\textsf{cat}}$ for the syntactic category (of contexts and substitutions) associated to the preceding type theory, with rules (6) and (7) for introducing coherences, we propose the following definition.

Definition 46**.**

An $\omega$-category is a set-theoretic model of $\mathcal{S}_{\textsf{cat}}$.

IV-C The Grothendieck-Maltsiniotis definition

In order to motivate our definition on the theoretical side, we briefly recall the Grothendieck-Maltsiniotis definition of $\omega$-categories in next section and conjecture that it coincides with our definition, see [13] and [2] for details.

Fix a globular extension $\mathbf{G}\to\mathcal{C}$. A morphism $f$ in $\mathcal{C}$ is algebraic when for every decomposition $f=g\circ f^{\prime}$ with $g$ globular, $g$ is an identity. From a proof-theoretic perspective, this means that $f$ cannot be obtained by non-trivially weakening another morphism $f^{\prime}$, i.e. it “uses” all the cells in its source (requirements below that some morphisms should be algebraic will give rise to the side conditions of our rules). A pair of morphisms

[TABLE]

is parallel when $i>0$ implies

[TABLE]

A lifting for such a pair is a morphism $h:D_{i+1}\to X$ such that $f=h\circ\sigma_{i}$ and $g=h\circ\tau_{i}$:

[TABLE]

A pair of parallel morphisms as above is admissible when either

there exist decompositions

[TABLE]

with $f^{\prime}$ and $g^{\prime}$ algebraic, or 2. 2.

$f$ and $g$ are algebraic.

The canonical coherator for $\omega$-categories, written $\mathbf{\Theta}$, is the colimit of the diagram of globular extensions

[TABLE]

where $\mathbf{\Theta}_{i+1}$ is the globular extension obtained from $\mathbf{\Theta}_{i}$ by formally adding a lifting for every admissible pair of arrows, and taking the globular extension freely generated by the resulting category (see Section III-A).

Definition 47** ([13]).**

An $\omega$-category $C$ is a functor $C:\mathbf{\Theta}^{\textnormal{op}}\to\mathbf{Set}$ such that $C^{\textnormal{op}}$ preserves globular sums.

The two rules (6) and (7) for introducing coherences in Section IV-B correspond precisely to formally adding lifting for admissible morphisms, with each rule corresponding to one of the conditions for being admissible. The details, however, are rather involved and left for future work.

Conjecture 48**.**

The category $\mathcal{S}_{\textsf{cat}}$ is equivalent to $\mathbf{\Theta}$.

More precisely, we define the coherence depth $\operatorname{cd}(t)$ of a term $t$ as the number of nested coherences, i.e. $\operatorname{cd}(x)=0$, $\operatorname{cd}(\mathsf{coh}_{\Gamma,A}\sigma)=\max(\operatorname{cd}(A)+1,\operatorname{cd}(\sigma))$, etc. Given $n\in\mathbb{N}$, we conjecture that the subcategory of $\mathcal{S}_{\textsf{cat}}$, with the same objects, morphisms being substitutions with coherence depth less than $n$, is equivalent to $\mathbf{\Theta}_{n}$. Finally, we conjecture that the situation wrt set-theoretic models described Section II-F generalizes as follows.

Conjecture 49**.**

*Type-theoretic $\omega$-categories (Definition 46) correspond precisely to Grothendieck-Maltsiniotis $\omega$-categories (Definition 47). *

V Implementation(s)

Since there are two authors for this paper, there are also two implementations of a type-checker for the theory. The first111https://github.com/ericfinster/catt is done in Haskell, following precisely the inference rules described in this article, while the other222https://github.com/smimram/catt is in OCaml and has some more experimental features (notably, the presence of implicit arguments making proofs much shorter but lacking theoretical justification for the moment). The second implementation may be tried online333https://smimram.github.io/catt.

In fact, our definition naturally lends itself to standard techniques for the implementation of a type checking algorithm for a dependent type theory, although in view of sparseness of the theory, these techniques appear in a rather simplified form. The Haskell implementation, for example, uses a simple bi-directional typechecking setup together with normalization by evaluation. Furthermore, while the theory lacks any notion of abstraction, the coherences are nonetheless assigned the type of a dependent product internally, allowing for substitution to propagate in the types. Indeed one sees immediately by inspection of the rules that each coherence can naturally be seen as a formal constant in the dependent product obtained by abstracting over all of the variables in the context (necessarily a pasting scheme) which defines it.

In our system, the user writes statements of the form

[TABLE]

and the typechecker automatically ensures that the judgment is derivable, or issues an error if it is not the case. In practice, coherences are written

[TABLE]

where $name$ allows the user to give a name to a coherence. Note that the order in which arguments are given is important, as it is used to determine whether the corresponding context is a ps-context or not. The arrow type $x\underset{A}{\to}y$ is noted

[TABLE]

For instance, we can define identities on [math]-cells:

coh id (x : *) : * | x -> x ;

composition of $1$-cells:

coh comp (x : *) (y : *) (f : * | x -> y) (z : *) (g : * | y -> z) : * | x -> z ;

left unitor:

coh unitl (x : *) (y : *) (f : * | x -> y) : * | x -> y | comp x x (id x) y f -> f ;

the “inverse” for left unitor:

coh unitl’ (x : *) (y : *) (f : * | x -> y) : * | x -> y | f -> comp x x (id x) y f ;

associativity of composition of $1$-cells:

coh assoc (x : *) (y : *) (f : * | x -> y) (z : *) (g : * | y -> z) (w : *) (h : * | z -> w) : * | x -> w | comp x z (comp x y f z g) w h -> comp x y f w (comp y z g w h) ;

vertical composition of $2$-cells:

coh vcomp (x : *) (y : *) (f : * | x -> y) (g : * | x -> y) (a : * | x -> y | f -> g) (h : * | x -> y) (b : * | x -> y | g -> h) : * | x -> y | f -> h ;

horizontal composition of $2$-cells:

coh hcomp (x : *) (y : *) (f : * | x -> y) (g : * | x -> y) (a : * | x -> y | f -> g) (z : *) (h : * | y -> z) (k : * | y -> z) (b : * | y -> z | h -> k) : * | x -> z | comp x y f z h -> comp x y g z k ;

the exchange law:

coh ichg (x : *) (y : *) (f : * | x -> y) (g : * | x -> y) (a : * | x -> y | f -> g) (h : * | x -> y) (b : * | x -> y | g -> h) (z : *) (l : * | y -> z) (m : * | y -> z) (c : * | y -> z | l -> m) (n : * | y -> z) (d : * | y -> z | m -> n) : * | x -> z | comp x y f z l -> comp x y h z n | hcomp x y f h (vcomp x y f g a h b) z l n (vcomp y z l m c n d) -> vcomp x z (comp x y f z l) (comp x y g z m) (hcomp x y f g a z l m c) (comp x y h z n) (hcomp x y g h b z m n d) ;

Finally, and as expected, defining an “inverse” for an arbitrary $1$-cell fails: the input

coh inv (x : *) (y : *) (f : * | x -> y) : * | y -> x ;

produces the following output:

Checking coherence: inv Valid tree context Src/Tgt check forced Source context: (x : *) Target context: (y : *) Failure: Source is not algebraic for y : *

meaning that the side conditions of the rule (6) are not fulfilled.

VI Conclusion and future work

We have presented a type theory designed to capture a well-known definition of $\omega$-category, extending work on a similar definition for $\omega$-groupoids. Most importantly, we have examined the relationship between pasting schemes represented as well-formed contexts, and their semantic counterparts (Batanin trees and globular sums). We conjecture that the models of this theory coincide with the definition of Maltsiniotis, but a detailed comparison will have to await further work.

We note also that the combinatorics of pasting schemes, as described by their $\triangleleft$-relation, seems promising. It quickly reminds one of the theory of Dyck words and we expect that interesting results can be obtained by applying similar methods.

Brunerie’s definition of $\omega$-groupoids, upon which this work builds, was of course motivated by the view of types advocated in homotopy type theory. Since the introduction of homotopy type theory [16], many authors have wondered about the possibility of weakening the equality relation in order to obtain a theory in which types behave as categories or directed homotopy types. We feel that the theory presented in this paper serves as a small step in this direction, isolating the core system of coherences which one would like to have. In future work, we aim to see if other type theoretic constructions ($\Sigma$ and $\Pi$ types, for example) may be reasonably added to the theory, thus increasing its expressive power.