---
abstract: 'We present a type theory for strictly unital $\infty$-categories, in which a term computes to its strictly unital normal form. Using this as a toy model, we argue that it illustrates important unresolved questions in the foundations of type theory, which we explore. Furthermore, our type theory leads to a new definition of strictly unital $\infty$-category, which we claim is stronger than any previously described in the literature.'
author:
- 'Eric Finster[^1] , David Reutter[^2]  and Jamie Vicary[^3]'
bibliography:
- 'references.bib'
subtitle: '*A Toy Model for the Identification Paradox*'
title: 'A Type Theory for Strictly Unital $\infty$-Categories'
---

Introduction
============

Overview
--------

§

#### Motivation

Standard categorical models of type theory have a curious and well-known feature. When we regard the $\lambda$-calculus as a presentation of a cartesian closed category, we must identify all $\beta$-equivalent terms, such as the following, $$(\lambda x.p)q = p[q/x]$$ by quotienting the set of raw syntactic terms by definitional equality, written “$=$”.

However, since any semantic model is required to respect definitional equality, it then becomes impossible for the semantics to represent the dynamics of computation in a nontrivial way. We call this the *Identification Paradox*. Like most good paradoxes, it does not represent a logical absurdity; after all, our standard models of type theory continue to serve us well for many purposes. Rather, it serves to challenge us, as we seek new perspectives on the foundations of computation.

In dependent type theories, the Identification Paradox gains greater weight, since it leads directly to a number well-known meta-theoretic difficulties. The conversion rule

allows us to silently coerce terms between two types which are equal up to definitional equality, but records no witness of this conversion in the syntax of the term $a$. For typing purposes, definitionally equal types have been *identified*. Such silent conversions can cause serious problems when we attempt to treat the meta-theory of type theory *in* type theory. For example, one extremely natural approach to modeling the syntax of type theory is as a sequence of inductive families: types dependent on contexts, terms dependent on types and so on [@chapman2009type; @danielsson2006]. However, in this case the “silent” conversion rule is not even type-correct: if we have two syntactically distinct type expressions, say $A$ and $A'$, then our meta-theory forbids the *same* term expression $a$ to have two *distinct* types, whatever our notion of definitional equality may be. Indeed, some kind of explicit coercion becomes necessary because of the proof-relevance of type theory itself. Various partial solutions are possible: working always with raw syntax, using setoids [@buisse2008towards], or more recently, using higher inductive types [@altenkirch2016type]. But it is fair to say that the meta-theory of type theory in a proof-relevant setting hides many subtleties which are not yet fully understood [@shulman2014homotopy]. We regard this situation as symptomatic of the Identification Paradox.

It was suggested already in the 1980s [@seely1987modelling] that ideas from *higher category theory* could be relevant to these questions. Put simply, while 1categorical structures require that we *identify* computationally-equivalent terms in the model, higher categorical structures allow us to retain the information of *why* these terms are equal by modelling them as *higher dimensional* equalities. While various authors have followed this kind of approach in low dimensions [@saville2019cartesian; @hilken1996towards], many basic foundational questions and difficulties still remain, and the Identification Paradox remains substantially unresolved.

$$\def\hrt{0.86602540378}
\tikzset{label/.style={opacity=0}}
\tikzset{extra/.style={densely dotted, thick}}
\begin{tikzpicture}[thick]
\draw [use as bounding box, draw=none] (-2.75,-2.5) rectangle +(4.05,5.5);

\node [label] (a) at (0,0) {a};
\node [label] (b) at (0,2*\hrt) {b};
\node [label] (c) at (-1.5,\hrt) {c};
\node [shift=(120:1), label] (0) at (a) {0};
\node [shift=(180:1), label] (1) at (a) {1};
\node [shift=(240:1), label] (2) at (a) {2};
\node [shift=(-60:1), label] (3) at (a) {3};
\node [shift=(0:1), label] (4) at (a) {4};
\node [shift=(60:1), label] (5) at (a) {5};
\node [shift=(0:1), label] (6) at (b) {6};
\node [shift=(60:1), label] (7) at (b) {7};
\node [shift=(120:1), label] (8) at (b) {8};
\node [shift=(180:1), label] (9) at (b) {9};
\node [shift=(120:1), label] (10) at (c) {10};
\node [shift=(180:1), label] (11) at (c) {11};
\node [shift=(240:1), label] (12) at (c) {12};

\draw (7.center) -- (1.center);
\draw (10.center) -- (6.center);
\draw (8.center) -- (4.center);
\draw (11.center) -- (5.center);
\draw (10.center) -- (2.center);
\draw (12.center) -- (4.center);
\draw (9.center) -- (6.center);
\draw (9.center) -- (3.center);
\draw (2.center) to (3.center) to (4.center) to (5.center) to (6.center) to (7.center) to (8.center) to (9.center) to (10.center) to (11.center) to (12.center) to (1.center);
\draw (9.center) -- (12.center);
\draw (2.center) -- (5.center);

\def\ge{1.3}
\node [shift=(240:\ge), label] (2') at (a) {2'};
\node [shift=(-60:\ge), label] (3') at (a) {3'};
\node [shift=(0:\ge), label] (4') at (a) {4'};
\node [, label] (5') at (-.5+\ge,\hrt) {5'};
\node [shift=(0:\ge), label] (6') at (b) {6'};
\node [shift=(60:\ge), label] (7') at (b) {7'};
\node [shift=(120:\ge), label] (8') at (b) {8'};
\node [shift=(120:\ge), label] (9') at (0) {9'};
\node [shift=(-120:\ge), label] (1') at (0) {1'};
\node [shift=(120:\ge), label] (10') at (c) {10'};
\node [shift=(180:\ge), label] (11') at (c) {11'};
\node [shift=(240:\ge), label] (12') at (c) {12'};
\draw [extra] (1.center) to (1'.center);
\draw [extra] (2.center) to (2'.center);
\draw [extra] (3.center) to (3'.center);
\draw [extra] (4.center) to (4'.center);
\draw [extra] (5.center) to (5'.center);
\draw [extra] (6.center) to (6'.center);
\draw [extra] (7.center) to (7'.center);
\draw [extra] (8.center) to (8'.center);
\draw [extra] (9.center) to (9'.center);
\draw [extra] (10.center) to (10'.center);
\draw [extra] (11.center) to (11'.center);
\draw [extra] (12.center) to (12'.center);

\node [anchor=west, red] at (-.8,2) {$\bullet {\color{black}u}$};
\node [anchor=west, red] at (-.4,1.1) {$\bullet {\color{black}v}$};

\node [align=center, font={\small\sf}] at (-.75,-2) {(a) The set $\tm(\S')$ with small \\definitional equality classes};

\end{tikzpicture}
\quad\qquad\quad
\begin{tikzpicture}[thick]
\draw [use as bounding box, draw=none] (-2.75,-2.5) rectangle +(4.05,5.5);

\node [label] (a) at (0,0) {a};
\node [label] (b) at (0,2*\hrt) {b};
\node [label] (c) at (-1.5,\hrt) {c};
\node [shift=(120:1), label] (0) at (a) {0};
\node [shift=(180:1), label] (1) at (a) {1};
\node [shift=(240:1), label] (2) at (a) {2};
\node [shift=(-60:1), label] (3) at (a) {3};
\node [shift=(0:1), label] (4) at (a) {4};
\node [shift=(60:1), label] (5) at (a) {5};
\node [shift=(0:1), label] (6) at (b) {6};
\node [shift=(60:1), label] (7) at (b) {7};
\node [shift=(120:1), label] (8) at (b) {8};
\node [shift=(180:1), label] (9) at (b) {9};
\node [shift=(120:1), label] (10) at (c) {10};
\node [shift=(180:1), label] (11) at (c) {11};
\node [shift=(240:1), label] (12) at (c) {12};
\draw (0.center) -- (1.center) -- (2.center) -- (3.center) -- (4.center) -- (5.center) -- (6.center) -- (7.center) -- (8.center) -- (9.center) -- (10.center) -- (11.center) -- (12.center) -- (1.center);
\draw (5.center) -- (0.center) -- (9.center);

\def\ge{1.3}
\node [shift=(240:\ge), label] (2') at (a) {2'};
\node [shift=(-60:\ge), label] (3') at (a) {3'};
\node [shift=(0:\ge), label] (4') at (a) {4'};
\node [shift=(0:\ge), label] (6') at (b) {6'};
\node [shift=(60:\ge), label] (7') at (b) {7'};
\node [shift=(120:\ge), label] (8') at (b) {8'};
\node [shift=(120:\ge), label] (10') at (c) {10'};
\node [shift=(180:\ge), label] (11') at (c) {11'};
\node [shift=(240:\ge), label] (12') at (c) {12'};
\draw [extra] (2.center) to (2'.center);
\draw [extra] (3.center) to (3'.center);
\draw [extra] (4.center) to (4'.center);
\draw [extra] (6.center) to (6'.center);
\draw [extra] (7.center) to (7'.center);
\draw [extra] (8.center) to (8'.center);
\draw [extra] (10.center) to (10'.center);
\draw [extra] (11.center) to (11'.center);
\draw [extra] (12.center) to (12'.center);

\node [anchor=west, red] at (-.8,2) {$\bullet {\color{black} \pi(u)}$};
\node [anchor=west, red] at (-.4,1.1) {$\bullet {\color{black} \pi(v)}$};

\node [align=center, font={\small\sf}] at (-.75,-2) {(b) The set $\tm(\S)$ with large \\definitional equality classes};

\end{tikzpicture}$$

#### A New Paradigm

We now describe a novel approach to resolving the Identification Paradox, illustrated in Figures \[fig:hexagons1\] and \[fig:hexagons2\]. We begin by supposing a traditional type theory $\S$ as above, and we seek to construct an auxiliary type theory $\S'$, with a projection function $\pi : \tm(\S') \to \tm(\S)$ on valid syntactic terms that *preserves* definitional equality, but does not *reflect* it, for all $u,v \in \tm(\S')$:

-   $u =_{\S'} v \quad\Rightarrow\quad \pi(u) =_\S \pi(v)$

-   $u =_{\S'} v \quad\not\Leftarrow\quad \pi(u) =_\S \pi(v)$

This says intuitively that the auxiliary theory $\S'$ is more *fine-grained*, with a weaker notion of definitional equality, conveyed in Figure \[fig:hexagons1\] by the small triangles in part (a), compared to the large hexagons in part (b). In particular, we may find some $u,v \in \tm(\S')$ with $u \neq_{S'} v$, but $\pi(u) =_S \pi(v)$, indicated in Figure \[fig:hexagons1\] by the points $u,v$ in different triangles in part (a), and their images $\pi(u) , \pi(v)$ in the same hexagon in part (b). Since definitional equality is finer in $\S'$, it may therefore have semantics in which $u,v$ are *distinct*, even thought their images in $\S$ are definitionally equivalent. Depending on the theory $\S$, this structure $(\S',\pi)$ could perhaps be obtained trivially, possibly by letting the theories have the same terms (with $\pi = \id$), but restricting the notion of definitional equality in $\S'$; that is the idea conveyed in Figure \[fig:hexagons1\], with the triangles and hexagons of parts (a) and (b) tiling the same space, and $u,v$ drawn at the same positions as $\pi(u), \pi(v)$ respectively.

The crux of the idea is then the following. We may also seek a function $\rho:\tm(\S) \to \tm(\S')$ which *preserves and reflects* definitional equality, and which is *cancelled* by $\pi$ up to definitional equality, for all $p,q \in \tm(\S)$:\[rhoaxioms\]

-   $p =_\S q \quad\Leftrightarrow\quad \rho(p) =_{\S'} \rho(q)$

-   $\pi(\rho(p))=_\S p$

This says intuitively that $\rho$ encodes terms of $\S$ as terms of $\S'$, in a way which is faithful to their computational interpretation, in such a way that the original definitional equality class can be recovered. It may be surprising that this is possible, since we argued above that $\S'$ had a strictly *weaker* notion of definitional equality than $\S$. The conclusion is that the encoding $\rho$ must be nontrivial, allowing the ‘broad’ definitional equality classes of $\S$ to embed in the ‘narrow’ definitional equality classes of $\S'$.

$$\def\hrt{0.86602540378}
\tikzset{label/.style={opacity=0}}
\tikzset{extra/.style={densely dotted, thick}}
\begin{tikzpicture}[thick]
\draw [use as bounding box, draw=none] (-2.75,-2.5) rectangle +(4.05,5.5);

\node [label] (a) at (0,0) {a};
\node [label] (b) at (0,2*\hrt) {b};
\node [label] (c) at (-1.5,\hrt) {c};
\node [shift=(120:1), label] (0) at (a) {0};
\node [shift=(180:1), label] (1) at (a) {1};
\node [shift=(240:1), label] (2) at (a) {2};
\node [shift=(-60:1), label] (3) at (a) {3};
\node [shift=(0:1), label] (4) at (a) {4};
\node [shift=(60:1), label] (5) at (a) {5};
\node [shift=(0:1), label] (6) at (b) {6};
\node [shift=(60:1), label] (7) at (b) {7};
\node [shift=(120:1), label] (8) at (b) {8};
\node [shift=(180:1), label] (9) at (b) {9};
\node [shift=(120:1), label] (10) at (c) {10};
\node [shift=(180:1), label] (11) at (c) {11};
\node [shift=(240:1), label] (12) at (c) {12};
\draw (0.center) -- (1.center) -- (2.center) -- (3.center) -- (4.center) -- (5.center) -- (6.center) -- (7.center) -- (8.center) -- (9.center) -- (10.center) -- (11.center) -- (12.center) -- (1.center);
\draw (5.center) -- (0.center) -- (9.center);

\def\ge{1.3}
\node [shift=(240:\ge), label] (2') at (a) {2'};
\node [shift=(-60:\ge), label] (3') at (a) {3'};
\node [shift=(0:\ge), label] (4') at (a) {4'};
\node [shift=(0:\ge), label] (6') at (b) {6'};
\node [shift=(60:\ge), label] (7') at (b) {7'};
\node [shift=(120:\ge), label] (8') at (b) {8'};
\node [shift=(120:\ge), label] (10') at (c) {10'};
\node [shift=(180:\ge), label] (11') at (c) {11'};
\node [shift=(240:\ge), label] (12') at (c) {12'};
\draw [extra] (2.center) to (2'.center);
\draw [extra] (3.center) to (3'.center);
\draw [extra] (4.center) to (4'.center);
\draw [extra] (6.center) to (6'.center);
\draw [extra] (7.center) to (7'.center);
\draw [extra] (8.center) to (8'.center);
\draw [extra] (10.center) to (10'.center);
\draw [extra] (11.center) to (11'.center);
\draw [extra] (12.center) to (12'.center);

\draw [red, ->, shorten <=4pt, shorten >=4pt] (-.5,.5+2*\hrt) node {$\bullet$} to [out=down, in=75] node [right, pos=.7] {$f$} (-1,\hrt+.3) node [] {$\bullet$};

\draw [red, ->, shorten <=4pt, shorten >=4pt] (-.95,.5) node {$\bullet$} to [out=-50, in=-130] node [above, pos=.35] {$g$} (.5,.4) node [] {$\bullet$};

\node [align=center, font={\small\sf}] at (-.75,-2) {(a) The term $f \cdot g$ in $\S$};

\end{tikzpicture}
\quad
\begin{tikzpicture}[thick]
\draw [use as bounding box, draw=none] (-2.75,-2.5) rectangle +(4.05,5.5);

\node [label] (a) at (0,0) {a};
\node [label] (b) at (0,2*\hrt) {b};
\node [label] (c) at (-1.5,\hrt) {c};
\node [shift=(120:1), label] (0) at (a) {0};
\node [shift=(180:1), label] (1) at (a) {1};
\node [shift=(240:1), label] (2) at (a) {2};
\node [shift=(-60:1), label] (3) at (a) {3};
\node [shift=(0:1), label] (4) at (a) {4};
\node [shift=(60:1), label] (5) at (a) {5};
\node [shift=(0:1), label] (6) at (b) {6};
\node [shift=(60:1), label] (7) at (b) {7};
\node [shift=(120:1), label] (8) at (b) {8};
\node [shift=(180:1), label] (9) at (b) {9};
\node [shift=(120:1), label] (10) at (c) {10};
\node [shift=(180:1), label] (11) at (c) {11};
\node [shift=(240:1), label] (12) at (c) {12};

\draw (7.center) -- (1.center);
\draw (10.center) -- (6.center);
\draw (8.center) -- (4.center);
\draw (11.center) -- (5.center);
\draw (10.center) -- (2.center);
\draw (12.center) -- (4.center);
\draw (9.center) -- (6.center);
\draw (9.center) -- (3.center);
\draw (2.center) to (3.center) to (4.center) to (5.center) to (6.center) to (7.center) to (8.center) to (9.center) to (10.center) to (11.center) to (12.center) to (1.center);
\draw (9.center) -- (12.center);
\draw (2.center) -- (5.center);

\def\ge{1.3}
\node [shift=(240:\ge), label] (2') at (a) {2'};
\node [shift=(-60:\ge), label] (3') at (a) {3'};
\node [shift=(0:\ge), label] (4') at (a) {4'};
\node [, label] (5') at (-.5+\ge,\hrt) {5'};
\node [shift=(0:\ge), label] (6') at (b) {6'};
\node [shift=(60:\ge), label] (7') at (b) {7'};
\node [shift=(120:\ge), label] (8') at (b) {8'};
\node [shift=(120:\ge), label] (9') at (0) {9'};
\node [shift=(-120:\ge), label] (1') at (0) {1'};
\node [shift=(120:\ge), label] (10') at (c) {10'};
\node [shift=(180:\ge), label] (11') at (c) {11'};
\node [shift=(240:\ge), label] (12') at (c) {12'};
\draw [extra] (1.center) to (1'.center);
\draw [extra] (2.center) to (2'.center);
\draw [extra] (3.center) to (3'.center);
\draw [extra] (4.center) to (4'.center);
\draw [extra] (5.center) to (5'.center);
\draw [extra] (6.center) to (6'.center);
\draw [extra] (7.center) to (7'.center);
\draw [extra] (8.center) to (8'.center);
\draw [extra] (9.center) to (9'.center);
\draw [extra] (10.center) to (10'.center);
\draw [extra] (11.center) to (11'.center);
\draw [extra] (12.center) to (12'.center);

\draw [red, ->, shorten <=4pt, shorten >=4pt] (-.5,.5+2*\hrt) node {$\bullet$} to [out=down, in=75] node [right, pos=.7] {$\rho(f)$} (-1,\hrt+.3) node (X) {$\bullet$};

\draw [red, ->, shorten <=4pt, shorten >=4pt] (-.95,.5) node (Y) {$\bullet$} to [out=-50, in=-130] node [above, pos=.35] {$\rho(g)$} (.5,.4) node [] {$\bullet$};

\draw [green!80!black, ->, shorten <=4pt, shorten >=4pt, bend right] (X.center) to node [left] {$\phi$} (Y.center);

\node [align=center, font={\small\sf}] at (-.75,-2) {(b) The term $\rho(f \cdot g)$ in $\S'$};
\end{tikzpicture}
\quad
\begin{tikzpicture}[thick]
\draw [use as bounding box, draw=none] (-2.75,-2.5) rectangle +(4.05,5.5);

\node [label] (a) at (0,0) {a};
\node [label] (b) at (0,2*\hrt) {b};
\node [label] (c) at (-1.5,\hrt) {c};
\node [shift=(120:1), label] (0) at (a) {0};
\node [shift=(180:1), label] (1) at (a) {1};
\node [shift=(240:1), label] (2) at (a) {2};
\node [shift=(-60:1), label] (3) at (a) {3};
\node [shift=(0:1), label] (4) at (a) {4};
\node [shift=(60:1), label] (5) at (a) {5};
\node [shift=(0:1), label] (6) at (b) {6};
\node [shift=(60:1), label] (7) at (b) {7};
\node [shift=(120:1), label] (8) at (b) {8};
\node [shift=(180:1), label] (9) at (b) {9};
\node [shift=(120:1), label] (10) at (c) {10};
\node [shift=(180:1), label] (11) at (c) {11};
\node [shift=(240:1), label] (12) at (c) {12};
\draw (0.center) -- (1.center) -- (2.center) -- (3.center) -- (4.center) -- (5.center) -- (6.center) -- (7.center) -- (8.center) -- (9.center) -- (10.center) -- (11.center) -- (12.center) -- (1.center);
\draw (5.center) -- (0.center) -- (9.center);

\def\ge{1.3}
\node [shift=(240:\ge), label] (2') at (a) {2'};
\node [shift=(-60:\ge), label] (3') at (a) {3'};
\node [shift=(0:\ge), label] (4') at (a) {4'};
\node [shift=(0:\ge), label] (6') at (b) {6'};
\node [shift=(60:\ge), label] (7') at (b) {7'};
\node [shift=(120:\ge), label] (8') at (b) {8'};
\node [shift=(120:\ge), label] (10') at (c) {10'};
\node [shift=(180:\ge), label] (11') at (c) {11'};
\node [shift=(240:\ge), label] (12') at (c) {12'};
\draw [extra] (2.center) to (2'.center);
\draw [extra] (3.center) to (3'.center);
\draw [extra] (4.center) to (4'.center);
\draw [extra] (6.center) to (6'.center);
\draw [extra] (7.center) to (7'.center);
\draw [extra] (8.center) to (8'.center);
\draw [extra] (10.center) to (10'.center);
\draw [extra] (11.center) to (11'.center);
\draw [extra] (12.center) to (12'.center);

\draw [red, ->, shorten <=4pt, shorten >=4pt] (-.5,.5+2*\hrt) node {$\bullet$} to [out=down, in=75] node [right, pos=.7] {$f$} (-1,\hrt+.3) node [] {$\bullet$};

\draw [red, ->, shorten <=4pt, shorten >=4pt] (-.95,.5) node {$\bullet$} to [out=-50, in=-130] node [above, pos=.35] {$g$} (.5,.4) node [] {$\bullet$};

\draw [green!80!black, ->, shorten <=4pt, shorten >=4pt, bend right] (X.center) to node [left] {$\phi$} (Y.center);

\node [align=center, font={\small\sf}] at (-.75,-2) {(c) The term $\pi(\rho(f \cdot g))$ in $\S$};

\end{tikzpicture}$$

If we can equip a type theory $\mathsf{S}$ with this structure $(\S',\pi, \rho)$, it gives us a way to alleviate the Identification Paradox as follows, which we illustrate in Figure \[fig:hexagons2\]. Suppose $\S$ is a dependent type theory with types $U,V,W,T$, with $V$ fibred over $T$; then for any $t:T$, we have that $V[t]$ is a type. Now suppose we have function types and $g:V[t'] \to W$ in the theory $\S$, with $t =_\S t'$. Then the type checker will admit that $V[t]=V[t']$ definitionally, and hence that their composite $f \,\cdot g$ is a valid term in $\S$ by “silent coercion”, illustrated in part (a) of the figure; while the target of $f$ does not agree with the source of $g$, since these points are in the same definitional equality class, the type checker for $\S$ will certify the composite as well-typed. We may embed $f \cdot g$ into $\S'$ to obtain the valid term $\rho(f \cdot g)$, illustrated in part (b), where we may inspect it with the finer-grained semantics of $\S'$ to see in detail the mechanics of the coercion between $V[t]$ and $V[t']$, previously invisible in $\S$, but now manifested as a green arrow $\phi$. We may then project it back into $\S$ as $\pi(\rho(f \cdot g))$, obtaining a term which is not syntactically identical to the original term $f \cdot g$, but guaranteed to be definitionally equal to it.

One might then ask, if the fine-grained type theory $\S'$ is so much more expressive, why should we bother with $\S$ at all? The simple answer is that $\S'$ may be *much harder* to work with in practice. The smaller definitional equality classes mean that type coercions may not be admitted automatically by the type checker, and must be added ‘by hand’ when needed. We see this illustrated clearly in Figure \[fig:hexagons2\]. In part (a) the terms $f,g$ are composable, since the head of $f$ is in the same definitional equivalence class as the tail of $g$. But in part (b) they are *not* directly composable, since the head of $\rho(f)$ is in a different definitional equality class to the source of $\rho(g)$; we require the insertion of the explicit coercion $\phi$ to allow the composite to be formed. While in this instance we constructed $\rho$ algorithmically through the encoding procedure $\rho$, if we only had access to the fine-grained theory $\S'$, we would need to construct it explicitly. The best scenario is to allow ourselves access to *both* $\S$ and $\S'$, so we can work in $\S$ for convenience, then pass to $\S'$ when we need more detail about the explicit coercions at play.

#### Our contribution.

We give a comprehensive analysis of a solution to the Identification Paradox along the lines just described, from the perspective of a “toy model”, a type theory for weak $\infty$categories. At the same time, our results are of independent interest for the theory of weak $\infty$categories itself, leading to a new stronger definition of *strictly unital $\infty$category*[^4] than any previously given, and showing the potential impact of type-theoretical approaches to this area of pure mathematics. We summarize our specific contributions as follows.

-   For our fine-grained theory $\S'$ we choose $\Catt$, a dependent type theory recently introduced [@Finster2017] to describe weak $\infty$categories. Set-theoretic models[^5] of correspond to particular weak $\infty$categories, and a valid typing judgement $\Gamma \vdash t :A$ can be interpreted as the assertion “in the free weak $\infty$category generated by $\Gamma$, the term $t$ represents a morphism in the hom-set $A$”.

    The “programs” of this type theory have the curious feature of always being in normal form: they don’t “compute” anything at all, and hence the theory has no notion of definitional equality, beyond syntactic equality. The theory is in this sense *maximally* fine-grained. Nonetheless, the theory *describes* something highly nontrivial: the mathematics of weak $\infty$categories.

-   For our coarse-grained theory $\S$ we choose $\Catt_\su$, a dependent type theory for strictly unital $\infty$categories, presented here for the first time. As a type theory, it has the interesting property of being identical to $\Catt$, except for the introduction of a nontrivial notion of definitional equality. This type theory yields a new definition of strictly unital $\infty$category, as a set-theoretic model of $\Catt_\su$. In this theory, definitional equality of terms $t=t'$ can be interpreted as the assertion that the higher-categorical composites represented by $t$ and $t'$ differ only in their unit structure.

-   We give a detailed analysis of definitional equality in $\Catt_\su$, exhibiting a reduction strategy which produces for every term $t$ a normal form $N(t)$. We show that our reduction strategy generates definitional equality, meaning $t = t'$ if and only if $N(t)$ and $N(t')$ are syntactically identical up to $\alpha$equivalence. Definitional equality is hence decidable, and the type theory can be implemented.[^6]

-   We show that valid $\Catt_\su$ terms over disc contexts trivialize, yielding strong evidence that our definition of strictly unital $\infty$category is directly comparable, and likely stricter, than previous work (see Related Work section below.)

-   The raw syntax of $\Catt$ and $\Catt_\su$ is identical, and the type checker of $\Catt_\su$ is strictly more permissive than that of $\Catt$, so the identity function serves as the projection $\pi : \tm(\Catt) \to \tm(\Catt_\su)$, which preserves but does not reflect definitional equality, as required.

-   By showing in $\Catt_\su$ that every term $t$ is *equivalent* to its normalization $N(t)$, we construct an encoding function $\rho: \tm(\Catt_\su) \to \tm(\Catt)$, satisfying the axioms given on page  above. This encoding function algorithmically inserts explicit coercions, which we can inspect directly in , providing a full solution to the Identification Paradox for this toy model.

Related work {#sec:relatedwork}
------------

#### Homotopy Type Theory

While our work is not directly concerned with Homotopy Type Theory [@hottbook], it is nonetheless heavily inspired by some of the developments that these ideas have provoked in the type theory community. Indeed, the definition of $\infty$-category presented in [@Finster2017], and developed in the present work, was based on a similar definition of $\infty$-groupoid [@brunerie2016homotopy]. And this definition in turn can be seen as a distillation of exactly that part of Martin-Löf’s identity elimination principle which causes types to behave as higher-dimensional groupoids.

A second point of contact between our work and Homotopy Type Theory is with respect to the problem of defining algebraic structures in a proof-relevant setting. The subtleties of this question are well known to mathematicians [@leinster2004higher; @boardman2006homotopy]. They arise from the observation that, when equality is rendered proof-relevant, the axioms of an algebraic theory may no longer be regarded as *properties* but rather themselves constitute additional *structure*. And in order to arrive at theories which are well behaved, we must then impose axioms *on the axioms* (so-called coherence conditions). The end result is that the proof-relevant versions of even the most common algebraic structures (e.g. monoids, groups, rings) become infinite dimensional. As an illustration of the difficulties this poses, it remains an open question in Homotopy Type Theory how to define even the correct proof-relevant notion of *category*. While we do not attack this problem directly in this paper, this work may be regarded as a kind of study in the presentation of higher dimensional structures, and we hope that some of the techniques and ideas may prove useful in the future.

Finally, while importing ideas from homotopy theory has proven fruitful for our understanding of the proof-relevant equality of type theory, we feel that, conversely, ideas from logic and computer science may also lead to progress in thinking about higher dimensional structures, along the lines of the unification of physics, topology and logic envisioned in [@baez2010physics]. Indeed, while mathematicians typically treat higher categorical structures starting from *combinatorial* descriptions of their underlying data (for example, using *simplices*, as in [@lurie2009higher]), the emerging connections with logic suggest a possible way of thinking of these structures *syntactically*, an approach closer to that of universal algebra. This paper is an example of this line of thought, where we apply type theoretic ideas to the study of a particular structure, that of $\infty$-categories themselves.

#### Higher Category Theory

Higher category theory is today a significant part of the landscape of modern mathematics. Definitions of higher categories have a long history and, roughly speaking, come in two flavours: ‘homotopical’, where composition operations are not explicitly specified and compositions are only required to exist up to a contractible space of choices, and ‘algebraic’, where all composition operations and higher coherences between these are explicitly specified and given as part of the data of a higher category. A prominent representative of this algebraic style is Leinster’s variant [@leinster2004higher] of Batanin’s original definition [@Batanin98] of a weak $\infty$-category as an algebra over a certain globular operad.

Our work builds directly on, and extends, the type theory $\Catt$ [@Finster2017], the models of which yield an algebraic notion of weak $\infty$-category which agrees with a definition due to Maltsiniotis [@Maltsiniotis], which itself is a close cousin of Batanin’s and Leinster’s definitions (see [@Ara] for a direct comparison.)

The type theory $\Catt_{\su}$ considered in this paper is a quotient of the type theory $\Catt$ by a definitional equality relation, yielding a new notion of strictly unital weak $\infty$-category. A related definition of strictly unital weak $\infty$-category in the setting of Leinster’s contractible globular operads has been given by Batanin, Cisinski and Weber [@Batanin2013]. We expect our notion of strict unitality to be *stricter* than this previous definition, for the following reason. Their theory includes a notion of *reduction*, corresponding directly to our Theorem \[thm:disctrivialization\]; and also a notion of *unit compatibility*, corresponding directly to our <span style="font-variant:small-caps;">Prune</span> generator for definitional equality. However, one of our generators of definitional equality, which we call <span style="font-variant:small-caps;">Endo</span>, has no obvious counterpart in their work, and we give on page  an example of a pair of terms which are definitionally equal in $\Catt_\su$, but we believe would not be identified in BCW’s theory.

A prominent difficulty with traditional algebraic definitions of higher category arises from their complexity, with nontrivial computations requiring one to keep track of an abundance of higher-dimensional coherence data. However, a major open conjecture in the field is that much of this data is in fact *redundant*, leading to a search for “semi-strict” replacement theories, in which as much as possible of this coherence data is removed.[^7] Low-dimensional examples of such semi-strict theories are well known, with the theory of strict $2$-categories (which are equivalent to weak $2$-categories) and the theory of Gray-categories [@GPS] (which are equivalent to weak $3$-categories) thoroughly understood. A recent framework for a combinatorial theory of semi-strict higher categories, suitable for computer implementation, is described in [@Dorn; @ReutterVicary]; however, a disadvantage of that work is that its formal foundations are far from the standard algebraic definitions of Batanin, Leinster, Maltsiniotis and others. Our work seeks ultimately to bridge the gap between traditional algebraic definitions and these more modern combinatorial theories that are more useful in practice, and shows for the first time that type theory can be a powerful tool in this quest.

Outline
-------

The paper is structured as follows. In Section 2, we set up our type theory for $\infty$-categories, starting with a presentation along the lines of [@Finster2017], and then introducing a non-trivial definitional equality. Section 3 analyzes the resulting reduction relation and describes an algorithm for producing normal forms, proving these decide definitional equality. Section 4 describes a certain meta-theoretic property of the resulting system which shows its compatibility with other notions of strictly unital higher category. Finally, in Section 5 we describe our process of “rehydration”: starting from a term in our strictly unital theory, we lift this term to a term in the fully weak theory which normalizes to it.

#### Proofs

All proofs are given in the anonymous supplementary materials for the results we present.

The Type Theories $\Catt$ and $\Catt_{\su}$ {#sec:typetheory}
===========================================

It will be convenient to construct our theory in three layers. We begin with the raw syntax and basic rules for contexts, types and substitutions, leaving out the term forming rules. Most of this material is standard, and we make sure to point out any idiosyncracies of notation as we proceed. After introducing the notion of *pasting context* we then present the term forming structure of $\Catt$. Finally, we introduce some combinatorial material necessary to describe our equality relation on terms, culminating in the definition of the theory $\Catt_{\su}$.

The Base Theory 
----------------

#### Raw Syntax

We fix an infinite set $V$ of variables, and use lowercase Roman ($x,y,\dots$) and Greek ($\alpha, \beta, \ldots$) letters to refer to its elements. The raw syntax of $\Catt$ consists of four syntactic classes: *contexts*, *types*, *terms* and *substitutions* (denoted $\Ctx$, $\Type$, $\Term$ and $\Sub$, respectively). These classes are defined by the rules in Figure \[fig:syntax\]. Observe that both contexts and substitutions appear in the raw syntax of terms.

We write $\equiv$ for syntactic equality of the various syntactic classes up to $\alpha$equivalence.

&\
&\
&\
&

#### Free Variables

The *free variables* of elements of each syntactic class are defined by induction on the structure as $$\begin{aligned}
  \FV(\emptyset) &= \emptyset & \FV(\star) &= \emptyset \\*
  \FV(\Gamma, x : A) &= \FV(\Gamma) \cup \{ x \} & \FV(s \to_A t) &= \FV(A) \cup \FV(s) \cup \FV(t) \\[5pt]
  \FV(x) &= \{ x \} \hspace{2ex} \text{for $x \in V$} & \FV(\langle \rangle) &= \emptyset \\ 
  \FV(\coh(\Gamma : A)[\sigma]) &= \FV(\sigma) & \FV(\langle \sigma , x \mapsto t \rangle) &= \FV(\sigma) \cup \FV(t) \\
\intertext{
\paragraph{Dimension}We define the \emph{dimension} of a type by
induction:}
\dim \, \star &= -1 & \dim \, (s \to_A t) &= \dim \, A + 1
\intertext{We extend this notion to contexts by asserting that the dimension of a
context is one more than the maximum of the dimension of the types
occurring in that context.}
  \dim \, \emptyset &= -1 &\dim \, (\Gamma, x : A) &= \max(\dim \, \Gamma , \dim \, A + 1)
\intertext{\paragraph{Identity Substitutions}For a context $\Gamma$, we
write $\id_{\Gamma}$ for the identity substitution on $\Gamma$
defined by}
  \id_{\emptyset} &= \langle \rangle & \id_{\Gamma, x : A} &= \langle \id_{\Gamma}, x \mapsto x \rangle\end{aligned}$$

#### Term Substitutions and Compositions

Although the terms of $\Catt$ are always in normal form, we will need to perform actual substitutions on terms during type-checking. We therefore also define a semantic form of substitution which calculates by induction on the structure of terms. We denote this operations by $\sub{-}$ in order to distinguish if from the $[-]$ appearing in coherence terms, which is part of the syntactic structure. This operation is defined as follows: $$\begin{aligned}
  \star\sub{\sigma} &= \star \\*
  (s \to_{A} t)\sub{\sigma} &=  s\sub{\sigma} \to_{A\sub{\sigma}} t\sub{\sigma} \\*
  \coh (\Gamma : s \to t)[\tau]\sub{\sigma} &= \coh (\Gamma : s \to t)[\tau \circ \sigma] \\*
  x\sub{\sigma} &= t \qquad \text{if $x \mapsto t \in \sigma$}  \\\end{aligned}$$ where the composition of substitutions ($\circ$) is defined mutually recursively as $$\begin{aligned}
  \langle \rangle \circ \sigma &= \langle \rangle
  &
  \langle \tau , t \rangle \circ \sigma &= \langle \tau \circ \sigma , t\sub{\sigma} \rangle\end{aligned}$$

With the previous material in place, our basic typing judgements for contexts, types and substitutions are given in Figure \[fig:basic-rules\]. The rules are standard for a dependent type theory. Note that our types consist of just a single base type denoted $\star$ and a formation rule analogous to the formation rule for identity types in Martin Löf Type Theory. The fact that this rule captures faithfully the notion of globular set is at the heart of the connection between type theory and higher category theory, and is the basis of this syntactic description of $\infty$-categories.

&\
&\
&

#### Support

Given a term $t : \Term$ and a type $A : \Type$, we can define the *support* of $t$ and $A$ to be the union of their free variables. That is $$\supp(t, A) = \FV(t) \cup \FV(A)$$ In practice, we will only use this definition when we are given a context $\Gamma$ and we have $\Gamma \vdash t : A$. When $\Gamma$ and $A$ are clear from the context, we will often simply write $\supp(t)$ and refer to this as the support of $t$.

#### Pasting Contexts

The terms of $\Catt$ are derived from isolating a distinguished subset of contexts which we call *pasting contexts*. A set of rules for exhibiting evidence that a given context is a pasting context was the key innovation of [@Finster2017]. These rules are presented in Figure \[fig:ps-rules\].

&\
&

#### Boundary Variables

For each pasting context $\Gamma \vdash_{p}$, we will define two distinguished subsets of the variables, denoted $\partial^-(\Gamma)$ and $\partial^+(\Gamma)$. First, for a variable $x : A \in \Gamma$, define its dimension to be $\dim A + 1$. Furthermore, let us say that a variable is *target-free* if it does *not* occur as the target of any other variables in $\Gamma$. Similarly, we have the notion of *source-free*. We now define: $$\begin{aligned}
  \partial^-(\Gamma) &:= \{ x \in \Gamma \, | \, \dim \, x < \dim \, \Gamma - 1 \textit{, or, } \dim \, x = \dim \, \Gamma - 1 \, \text{and $x$ is target-free} \} 
\\
  \partial^+(\Gamma) &:= \{ x \in \Gamma \, | \, \dim \, x < \dim \, \Gamma - 1 \textit{, or, } \dim \, x = \dim \, \Gamma - 1 \, \text{and $x$ is source-free} \} \end{aligned}$$

#### Terms

With these notions in place, the typing rules for terms of $\Catt$ are shown in Figure \[fig:terms\]. Note that when writing the substitution in a coherence term, we typically omit the angled brackets, writing $\coh(\Gamma : s \to_A t)[a, b, c, \dots]$ instead of $\coh(\Gamma : s \to_A t)[\langle a, b , c, \dots \rangle]$.

#### Examples

We record here some basic examples of well-typed terms. In terms of the structure of an $\infty$-category, these terms represent, respectively: unary composition, binary composition, ternary composition, identities of objects, the right unit law, and a “padding” composition we will describe below. Note that we use parentheses for delineating our contexts here as it improves readability. $$\begin{aligned}
  \mathsf{comp_1} &:= \coh((x : \star)(y : \star)(f : x \to_\star y) : x \to_\star y)[x,y,f] \\[5pt]
  \mathsf{comp_2} &:= \coh((x : \star)(y : \star)(f : x \to_\star y) (z : \star)(g : y \to_\star z) : x \to_\star z)[x,y,f,z,g] \\[5pt]
  \mathsf{comp_3} &:= \coh((x : \star)(y : \star)(f : x \to_\star y) (z : \star)(g : y \to_\star z) \\[-2pt]
                  & \hspace{1.2cm} (w : \star)(h : z \to_\star w) : x \to_\star w)[x,y,f,z,g,w,h] \\[5pt]
  \i_0 &:= \coh((x : \star) : x \to_{\star} x)[x] \\[5pt]
  \mathsf{unit\mhyphen r} & := \coh((x : \star)(y : \star)(f : x \to_\star y) : \mathsf{comp_2}\sub{x,y,f,y,\i_0\sub{y}} \to_{x \to_\star y} f)[x,y,f] \\[5pt]
  \mathsf{comp_{2,0}} &:= \coh((x : \star)(y : \star)(f : x \to_\star y) (z : \star)(g : y \to_\star z) (h : y \to_\star z)(\alpha : g \to_{y \to_\star z} h) \\[-2pt]
                  & \hspace{1.2cm} (w : \star)(k : z \to_\star w) \\
                  & : \mathsf{comp_3}\sub{x,y,f,z,g,w,k} \to_{(x \to_\star w)} \mathsf{comp_3}\sub{x,y,f,z,h,w,k})[x,y,f,z,g,h,\alpha,w,k]
          $$ From the perspective of the theory of $\infty$categories, these all correspond to *operations* from low-dimensional higher category theory, such as the theory of bicategories. In that more familiar language, given objects $x,y,z,w$ and 1morphisms $f:x \to y$, $g :y \to z$, $h:z \to w$, we have the following, where we write $\cdot$ for forward composition of 1morphisms:

-   $\comp_2 \sub{ x, f, y, z, g}$ corresponds to the binary composite $f \cdot g$;

-   $\comp_3 \sub{x, y, f, z, g, w, h}$ corresponds to the unbiased ternary composite , which is not directly defined in the traditional notion of bicategory;

-   $\comp_2 \sub{x, \comp_2 \sub{x, f, y, z, g}, z, w, h}$ corresponds to the repeated binary composite $(f \cdot g) \cdot h$;

-   $\i_0 \sub x$ corresponds to the 1morphism $\id_x$;

-   $\mathsf{unit\mhyphen r} \sub f$ corresponds to the invertible 2morphism $f \cdot \id_x \Rightarrow f$.

We could similarly write down operations for other familiar operations in the theory of weak $\infty$categories, such as associators, interchangers, and so on, in principle in all dimensions. It is in this sense that gives a formal language for weak $\infty$categories. More examples are given in [@Finster2017].

This last example $\comp_{2,0}$ is part of a family of coherences $\mathsf{comp_{d,k}}$ for $k < d$, \[page:comp\]which will play a role in Section \[sec:rehydration\]. While we will not give a formal definition, these compositions can be described intuitively as follows: they consist of the “unbiased” composite of a $d$-dimensional disc $D$ with two $(k+1)$-dimensional discs $S$ and $T$ glued to the $k$-dimensional source and target of $D$, respectively. We might write this composite intuitively, as follows: $$S \circ_{k} D \circ_{k} T$$

#### Identity Terms

Generalizing the 0-dimensional case above, we can define an identity on cells of arbitrary dimension. To do so, we assume that the set $V$ of variables contains elements $d_i$ and $d_i'$ for $i \in \N$. Now define the *$k$-disc context* and the *$(k-1)$-sphere type* by mutal induction on $k$ as follows: $$\begin{aligned}
  \uD^0 &:= \emptyset , d_0 : S^{-1} & S^{-1} &:= \star \\
  \uD^{k+1} &:= \uD^k, (d_k' : S^{k-1}) , (d_{k+1} : S^k) & S^{k} &:= d_k \to_{S^{k-1}} d_k' \end{aligned}$$ Finally, for $k \in \N$, we define the *identity on the $k$disc*, written $\i_k$ as $$\i_k := \coh ( \uD^k: d_k \to_{S^{k-1}} d_k)[\id _{D^k}]$$ One easily checks that this is a valid term in the context $\uD^k$.

The type theory $\Catt_\su$ {#sec:cattsu}
---------------------------

As described in the introduction, the type theory $\Catt$ of the previous section contains no non-trivial definitional equalities: while calculation happens during type-checking, all terms themselves are in normal form. In this section, we introduce our equality relation. Its definition will require some combinatorial preparation which we turn to now.

$$\tikzset{point/.style={draw, circle, black, fill, inner sep=1.5pt, label={}}}
    \begin{aligned}
      \begin{tikzpicture}[xscale=.6]
        \draw [use as bounding box, draw=none] (0,0) rectangle +(8,3);
        \draw (0,0) node [point] {} node [left] {$x$} to node [left] {$y$} node [right] {$f$} (1,1) node [point] {} to node [left] {$g$} node [right] {$\mu$} (2,2) node [point] {} to node [left] {$\nu$} node [right] {$\Omega$} (3,3) node [point] {} to (4,2) node [point] {} to (5,1) node [point] {} to node [left] {$h$} node [right] {$\delta$} (6,2) node [point] {} to (7,1) node [point] {};
      \end{tikzpicture}
    \end{aligned}$$

#### Labeled Dyck Words

Observe that each of the rules for pasting contexts in Figure \[fig:ps-rules\] has at most one hypothesis, and consequently, derivations made with these rules are necessarily linear. In fact, complete derivations of the fact that a context is a pasting context can be identified with *Dyck words* [@kozen2012automata]. While strictly speaking, a pasting context is defined as a pair of a syntactic context and a derivation of the fact that it is well-formed, this representation contains quite a bit redundancy and can be somewhat awkward to manipulate in practice. For the purposes of presentation, therefore, it is convenient to introduce a somewhat simplified representation of pasting diagrams which we call *labeled Dyck words*.

Labeled Dyck words may be pictured as a set of up and down moves, with each up move labeled by a pair of elements of some arbitrary labeling set $L$. Concretely, given $L$, the set $\LDyck \, L \, n$ of *labeled Dyck words of excess $n$* is defined by the rules given in Figure \[fig:dyck\] (in practice, we often omit $L$ from the notation as it will be clear from context). The parameter $n$ records the difference between the number of up moves and down moves. Note that the definition ensures that the excess is always non-negative, so that we always have at least as many up moves as down moves, leading to the “mountain” diagram shown in Figure \[fig:dyck-ex\].

When using labeled Dyck words to represent contexts, we take $L = V$, the set of variables. We hope the reader will notice how the rules for labeled Dyck words mirror exactly the derivation rules for pasting contexts of Figure \[fig:ps-rules\]. (The additional $\checkmark$ rule for pasting contexts forces a complete derivation $\Gamma \vdash_p$ to be of excess 0). As an example, consider the context $$(x : *) (y : *) (f : x \to_\star y) (z : *) (g : y \to_\star z)$$ It is proven to be a pasting context via the derivation

and its labeled Dyck word representation is $$\Downarrow \, (\Uparrow \, (\Downarrow \, (\Uparrow \, (\star \, x)
  \, y \, f) ) \,z \, g) ) : \LDyck \, V \, 0$$ Notice that the only difference between these two representations is that the pasting context, together with its derivation, remembers all the typing information of the all variables, while the Dyck word representation remembers just the variable names. Since the types can be recovered from the structure of the Dyck word itself, this represents no loss of information. In order to fix notation, if $\Gamma \vdash_p$ is a pasting context, we write $\lfloor \Gamma \rfloor : \LDyck \, 0$ for the corresponding labeled Dyck word and, conversely, for a Dyck word $d : \LDyck \, 0$, we write $\lceil d \rceil$ for the corresponding pasting context.

A nice advantage of this representation is that we can write programs on pasting contexts using pattern matching style (for which we will use an Agda-style syntax). As an example, consider the function $$\begin{aligned}
&\mathsf{flatten} : \{n : \N\} (d : \LDyck \, n) \to \List \, L
\intertext{extracting the list of labels.  This function can be defined as}
  &\mathsf{flatten} \, (\star x) = [x] \\
  &\mathsf{flatten} \, (\Uparrow \, d \, y \, f) = [\mathsf{flatten} \, d, y , f] \\
  &\mathsf{flatten} \, (\Downarrow \, d) = \mathsf{flatten} \, d\end{aligned}$$ We will make use of this function below.

#### Peaks

A special role will be played in what follows by the positions in a label Dyck word where we change direction from moving up to moving down. We call these the *peaks*. It is not hard to give an induction characterization of peaks, and we do so in Figure \[fig:peaks\].

We can use the definition of peaks to manipulate our Dyck word in various ways. Two operations which will be useful in what follows are *excising* a peak, and *replacing* the labels which occur at a given peak. The first operation has type $$\mathsf{excise} : \{n : \N\} (d : \LDyck \, n) (p : \Peak \, d) \to \LDyck \, n$$ and can be defined as $$\begin{aligned}
  &\mathsf{excise} \, \_ \, (\Updownarrow_{pk} \, d \, y \, f) = d \\
  &\mathsf{excise} \, \_ \, (\Uparrow_{pk} \, d \, y \, f \, p) = \Uparrow (\mathsf{excise} \, p) \, y \, f \\
  &\mathsf{excise} \, \_ \, (\Downarrow_{pk} \, d \, p) = \Downarrow (\mathsf{excise} \, p)\end{aligned}$$ The second operation is similar taking as arguments the new labels for the specified peak: $$\mathsf{replace} : \{n : \N\} (d : \LDyck \, n) (p : \Peak \, d) (g : L) (\alpha : L) \to \LDyck \, n$$ It is defined as $$\begin{aligned}
  &\mathsf{replace} \, \_ \, (\Updownarrow_{pk} \, d \, y \, f) \, g \, \alpha = \Downarrow (\Uparrow \, d \, g \, \alpha) \\
  &\mathsf{replace} \, \_ \, (\Uparrow_{pk} \, d \, y \, f \, p) \, g \, \alpha = \Uparrow (\mathsf{replace} \, p \, g \, \alpha) \, y \, f \\
  &\mathsf{replace} \, \_ \, (\Downarrow_{pk} \, d \, p) \, g \, \alpha = \Downarrow (\mathsf{replace} \, p \, g \alpha)\end{aligned}$$ A pictorial representation of the excision operation is given in Figure \[fig:excision\].

$$\tikzset{point/.style={draw, circle, black, fill, inner sep=1.5pt, label={}}}
    \begin{aligned}
      \begin{tikzpicture}[xscale=.6, scale=.8]
        \draw [use as bounding box, draw=none] (0,0) rectangle +(8,3);
        \draw (0,0) node [point] {} node [left=1pt] {$x$} to node [left] {$y\vphantom{yk}$} node [right] {$f\vphantom{yk}$} (1,1) node [point] {} to node [left] {$g\vphantom{yk}$} node [right] {$\alpha\vphantom{yk}$} (2,2) node [point] {} to (3,1) node [point] {} to node [left] {$h\vphantom{yk}$} node [right] {$\beta\vphantom{yk}$} (4,2) node [point] {} to (5,1) node [point] {} to (6,0) node [point] {} to node [left] {$z\vphantom{yk}$} node[right] {$k\vphantom{yk}$} (7,1) node [point] {} to (8,0) node [point] {};
        \draw [blue] (0.5,1) to +(3,0);
      \end{tikzpicture}
    \end{aligned}
    \quad\squig\quad
    \begin{aligned}
      \begin{tikzpicture}[xscale=.6, scale=.8]
        \draw [use as bounding box, draw=none] (0,0) rectangle +(6,3);
        \draw (0,0) node [point] {} node [left=1pt] {$x$} to node [left] {$y\vphantom{yk}$} node [right] {$f\vphantom{yk}$} (1,1) node [point] {} to node [left] {$h\vphantom{yk}$} node [right] {$\beta\vphantom{yk}$} (2,2) node [point] {} to (3,1) node [point] {} to (4,0) node [point] {} to node [left] {$z\vphantom{yk}$} node[right] {$k\vphantom{yk}$} (5,1) node [point] {} to (6,0) node [point] {};
      \end{tikzpicture}
    \end{aligned}$$

#### Locally Maximal Variables

If $\Gamma \vdash_p$ is a pasting context, we say that a variable which occurs as the label of a peak in the Dyck word representation of $\Gamma$ is *locally maximal*. Intuitively speaking, such variables represent those cells which are of highest dimension “in their neighborhood.” We write $\LM(\Gamma)$ for the set of locally maximal variables and for $\alpha \in \LM(\Gamma)$ we write $p_\alpha$ for the corresponding peak. Observe that if $\alpha \in \LM(\Gamma)$, we may speak of the *dimension* $\dim \, \alpha\,$ since $\alpha$ is assigned a type by $\Gamma$. Moreover, since all locally maximal variables are positive dimensional, any locally maximal variable $\alpha \in \LM(\Gamma)$ must be assigned an arrow type $\alpha : s \to_A t$ for some type $A$. In such a situation, we refer to $s$ as the *source* of $\alpha$ and to $t$ as its *target*, denoted $\src (\alpha)$ and $\tgt(\alpha)$ respectively.

Given a pasting context $\Gamma \vdash_p$ and a locally maximal variable $\alpha : \LM(\Gamma)$, we write $\Gamma\sslash \alpha$ for the pasting context obtained by excising the peak where $\alpha$ occurs in the Dyck word representation of $\Gamma$. $$\begin{aligned}
\Gamma\sslash \alpha &:= \lceil \mathsf{excise} \, \lfloor \Gamma
  \rfloor \, p_{\alpha} \rceil
  \intertext{There is a natural substitution
$\Gamma\sslash \alpha \vdash \pi_{\alpha} : \Gamma$ which may be
described as follows: regard $\lfloor \Gamma \rfloor$ as a Dyck
word labeled by \emph{terms} as opposed to merely variables.  Then
we can extract a substitution by replacing the label at the peak
$p_\alpha$ with an identity term as follows:}
\pi_\alpha &:= \lceil \mathsf{flatten} \, (\mathsf{replace} \,
  \lfloor \Gamma \rfloor \, p_\alpha \, (\src (\alpha)) \, \i_{\dim
    \alpha}) \rceil
\intertext{Finally, if $\Delta$ is another context, and we
are given a substitution $\Delta \vdash \sigma : \Gamma$, then we have
a substitution
$\Delta \vdash \sigma\sslash \alpha : \Gamma\sslash \alpha$ obtained
by merely dropping the terms assigned to the variables $\alpha$ and
$\tgt (\alpha)$,which are necessarily adjacent, from $\sigma$:}
\sigma &:= [ \ldots, \src(\alpha), \tgt(\alpha), \alpha, \ldots] \quad\Rightarrow\quad \sigma \dslash \alpha := [ \ldots, \src (\alpha), \ldots]\end{aligned}$$ In this case, the elements $t,\alpha$ are removed from the list to obtain the quotient substitution.

#### Unfolding Types

Given a type $T$, we obtain a list of terms $\{T\}$ as follows: $$\begin{aligned}
\{\star\} &:= []
&
\{ u \to_A v\} &:= [\{A\}, u, v]\end{aligned}$$ This is useful to define our endo-coherence removal relation below. We now prove a small lemma regarding type unfolding.

\[lem:typeunfoldingsub\] Substitution is compatible with type unfolding: $$\{T \sub \sigma \} \equiv \{T\} \circ \sigma$$

If $T \equiv \star$ then the lemma is vacuously true, since $\{\star\}$ is the empty list. If $T \equiv u \to_A v$, then we reason by induction on subtypes as follows: $$\begin{aligned}
\{ T \sub \sigma \} & \equiv \{(u \to_A v) \sub \sigma \}
\equiv [\{A \sub \sigma\}, u \sub \sigma, v \sub \sigma]
\equiv [\{A\}, u, v] \circ \sigma
\equiv \{u \to_A v\} \circ \sigma\end{aligned}$$ This completes the proof.

#### Equality in $\Catt_{\su}$

With these definitions in place, we can now define our equality relation on terms in Figure \[fig:eq-rules\]. There are three generating equalities, which we summarize as follows.

-   *Pruning* scans the locally maximal arguments of a substitution looking for identity terms. When such an argument appears, it may be removed while at the same time removing the corresponding locally maximal cell from the pasting diagram defining the coherence.

-   *Disc Removal* asserts that unary composites may be removed from the head of a term.

-   *Endomorphism Coherence Removal* asserts that coherences associated to a repeated term may be replaced with identities on that term.

From here, we extend this equality relation to contexts, types and substitutions by structural induction on the formations rules, and close these relations under reflexivity, symmetry and transitivity. As an example, the equality relation on types are shown in Figure \[fig:type-eq\]. Contexts, terms and substitutions are similar and we omit the details.

Finally, to integrate our new equality with the type system, we require all typing judgements to be equipped with conversion rules. These rules are listed in Figure \[fig:conversion\].

#### Example Reductions

We record here examples of our three generating reductions, in order to give the reader a flavour of how they operate.

#### $\bullet$ Pruning

The pruning relation is the workhorse of the theory, leading in practice to the richest algebraic phenomena. This relation says the following: if a coherence term has a substitution which sends a locally-maximal variable $\alpha$ to an identity, then $\alpha$ can be removed completely from the corresponding pasting context. Let us examine the behavior of this relation on the following term $$\begin{aligned}
    \mathsf{comp_2}\sub{x,y,f,y,\i_0\sub{y}} &:= 
    \coh((x : \star)(y : \star)(f : x \to_\star y) \\
    &\hspace{1.2cm} (z : \star)(g : y \to_\star z) : x \to_\star z)[x,y,f,y,\i_0\sub{y}]
  \end{aligned}$$ Observe that $g$ occurs in a locally maximal position in the head context: $$\Gamma  := (x : \star)(y : \star)(f : x \to_\star y) (z : \star)(g : y \to_\star z)$$ Moreover, the argument supplied in this position is $\i_0\sub{y}$. Hence the pruning relation applies. We have $$\begin{aligned}
    \Gamma\sslash g &:= (x : \star)(y : \star)(f : x \to_\star y) \\
    \pi_g &:= [x,y,f,y,\i_0\sub{y}] \\
    [x,y,f,y,\i_0\sub{y}]\sslash g &:= [x,y,f] \\
  \end{aligned}$$ so that this term is definitionally equal to the following: $$\coh((x : \star)(y : \star)(f : x \to_\star y) : x \to_\star y)[x,y,f]$$ \[ex:eq-exs\]

#### $\bullet$ Disc Removal

This relation can be summarized as follows: when the head of a coherence term has a certain form, the entire term is definitionally equal to the last argument of its substitution.

The result of the previous example may have been somewhat surprising: it would have been natural to expect that composing the arrow $f$ with an identity reduced to $f$ itself, whereas we have instead been left with a non-trivial coherence term. Upon closer inspection, we see that the resulting term can be considered the “unary composite” of $f$. The existence of these composites arise from the fact that our definition of $\infty$-category is *unbiased*: it allows (vertical) $n$-ary composites of cells for all $n$, including $n=1$. Our second definitional equality exactly removes these superfluous unary composites. In the case at hand, application of the <span style="font-variant:small-caps;">Disc</span> rule now yields: $$\coh((x : \star)(y : \star)(f : x \to_\star y) : x \to_\star
    y)[x,y,f] = f$$ Note that this replaces the coherence term with the final argument, $f$, of its substitution $[x, y, f]$. As $f$ is now a variable, the term is now in normal form (see Section 3).

#### $\bullet$ Endomorphism Coherence Removal

Another curious redundancy of the fully weak definition of $\infty$-category is the existence of “fake identities”: cells which are “morally” the identity on some composite cell, but do not have an identity coherence at their head. As an example, consider the term: $$\begin{aligned}
    &\coh((x : \star)(y : \star)(f : x \to_\star y)(z : \star)(g : y \to_\star z) \\
    &\hspace{.5cm} : \mathsf{comp_2}\sub{x,y,f,z,g} \to_{x \to_\star z} \mathsf{comp_2}\sub{x,y,f,z,g})[x,y,f,z,g] 
  \end{aligned}$$ This term is “trying” to be the identity on $\mathsf{comp_2}\sub{x,y,f,z,g}$ (it is, in fact, provably equivalent to it in $\Catt$), but is not actually a *syntactic* identity. Such terms are recognizable by the fact that they are coherences for which the type expression has a source and target which are equal. Henceforth we refer to them as *endomorphism coherences*, and our third rule <span style="font-variant:small-caps;">Endo</span> sets them equal to the identities they duplicate, in the case at hand $$\i_1\sub{x,z,\mathsf{comp_2}\sub{x,y,f,z,g}}$$ We point out that this third type of reduction has no apparent analog in the strictly unital theory of [@Batanin2013], which is otherwise closely related. \[ex:bcw\]

#### Properties of Definitional Equality

We record here some basic facts about the definitional equality relation of $\Catt_{\su}$ introduced above.

\[lem:quotientsub\] Composition of substitutions is compatible with taking quotients: $$(\mu \circ \sigma) \dslash \alpha = (\mu \dslash \alpha) \circ \sigma$$

\[lem:eq-sub-r-inv\] Let $\sigma, \sigma' : \Sub$ such that $\sigma = \sigma'$. For $A : \Type$ and $t : \Term$, we have: $$\begin{aligned}
    A\sub{\sigma} &= A\sub{\sigma'}
    &
    t\sub{\sigma} &= t\sub{\sigma'}
  \end{aligned}$$

Since substitution on types is given by structural induction (and the base case $A = \star$ is trivial), the first equation follows from the second.

Now, if $t$ is a variable, then the result is clear by the definition of equality on substitutions, which is just equality of the comprising terms. On the other hand, $t \equiv \coh(\Gamma : A)[\tau]$, then we are reduced to showing that $\tau \circ \sigma = \tau \circ \sigma'$ and this is clear by expanding the definition and applying the induction hypothesis.

\[lem:eq-sub-l-inv\] Let $\tau : \Sub$, $A, A' : \Type$ and $t, t' : \Term$. If $A = A'$ and $t = t'$, then: $$\begin{aligned}
    A\sub{\tau} &= A'\sub{\tau}
    &
    t\sub{\tau} &= t'\sub{\tau}
  \end{aligned}$$

As in the previous Lemma, the first statement follows from the second by just inducting on the structure of the equality relation on types.

For the second, we argue by induction on the structure of the proof that $t = t'$. It suffices to check the generating cases, as the rest will follow by structural induction and the reflexivity, symmetry and transitivity of $=$.

Hence, suppose we have $$t \equiv \coh(\Gamma : A)[\sigma] = \coh(\Gamma\sslash \alpha :
    A\sub{\pi_{\alpha}})[\sigma\sslash x] \equiv t'$$ Then we are reduced to showing that $ (\sigma \circ \tau)\sslash \alpha = (\sigma\sslash \alpha) \circ
  \tau$ which is Lemma \[lem:quotientsub\].

Next, if we have $$t \equiv \coh(\uD^{n+1} : S^n)[\sigma] = d_{n+1}\sub{\sigma} \equiv t'$$ we argue as follows: $$\begin{aligned}
    \coh(\uD^{n+1} : S^n)[\sigma]\sub{\tau} &= \coh(\uD^{n+1} : S^n)[\sigma \circ \tau] \\
                                            &= d_{n+1}\sub{\sigma \circ \tau} \\
                                            &= d_{n+1}\sub{\sigma}\sub{\tau}
  \end{aligned}$$

Finally, in the case that $$t \equiv \coh (\Gamma : t \to_A t)[\sigma] = \i_{\dim A+1}\sub{\{A\sub{\sigma}\}, t\sub{\sigma}} \equiv t'$$ we obtain $$\begin{aligned}
    \coh (\Gamma : t \to_A t)[\sigma]\sub{\tau} &= \coh (\Gamma : t \to_A t)[\sigma \circ \tau] \\
                                                &= \i_{\dim A+1}\sub{\{A\sub{\sigma \circ \tau}\}, t\sub{\sigma \circ \tau}} \\
                                                &= \i_{\dim A+1}\sub{\{A\sub{\sigma}\}, t\sub{\sigma}}\sub{\tau} \\
  \end{aligned}$$ where the last step follows from Lemma \[lem:typeunfoldingsub\].

\[uniquecohtype\] If $\Delta \vdash \coh(\Gamma : U)[\sigma] : A$ in $\Catt_{\su}$, then $A = U\sub{\sigma}$.

We induction on the structure of the derivation of $\Delta \vdash \coh(\Gamma : U)[\sigma] : A$. Since the term in question is not a variable, there are only two cases. If the derivation is simply the introduction rule for coherences, then the result is immediate, as $U\sub{\sigma}$ is the assigned type.

Otherwise, the proof must be by the use of the conversion rule for terms. In this case, we obtain some $\Delta'$, $A'$, $\Gamma'$, $U'$ and $\sigma'$ together with the obvious equalities between them. By the induction hypothesis, we have that $A' = U'\sub{\sigma'}$. And now, applying Lemmas \[lem:eq-sub-l-inv\] and \[lem:eq-sub-r-inv\] we have $$A = A' = U'\sub{\sigma'} =  U'\sub{\sigma} = U\sub{\sigma}$$ which completes the proof.

#### Inferred Types

We note that Proposition \[uniquecohtype\] guarantees that if $\Delta \vdash \coh(\Gamma:u \to_T v)[\sigma]:A$ is valid, then $A = (u\sub{\sigma} \to_{T\sub{\sigma}} v\sub{\sigma})$. So the type of a valid coherence term can be extracted from the syntax of the term itself up to definitional equality. We use this to define the *inferred type* of a coherence term, as follows: $$\begin{aligned}
\mathsf{ty}(\coh(\Gamma : U)[\sigma]) &:= U \sub\sigma
\intertext{Furthermore, we define the \textit{inferred source} and \textit{inferred target} as follows:}
\src(\coh(\Gamma : u \to_T v)[\sigma]) &:= u \sub \sigma
\\
\tgt(\coh(\Gamma : u \to_T v)[\sigma]) &:= v \sub \sigma\end{aligned}$$ We note that a term of the form $\coh(\Gamma : \star)[\ldots]$ is never valid, so $\src,\tgt$ are defined for every valid coherence term. Note that this notation is consistent with that introduced above for variables in a pasting context.

We also write $\src^k, \tgt^k$ for the iterated $k$fold inferred source or target, and $\src_k$, $\tgt_k$ for the $k$dimensional inferred source or target; so for a coherence term $t$ of dimension $n$, we have $\src_k(t) := \src^{n-k}(t)$, $\tgt_k(t) := \tgt^{n-k}(t)$.

Models of $\Catt$ and $\Catt_{\su}$ {#sec:models}
-----------------------------------

The type theories $\Catt$ and $\Catt_{\su}$ generate syntactic categories via a standard construction: objects are contexts, and morphisms are substitutions, up to definitional equality. Composition is given is via composition of substitutions. We abuse notation slightly and write $\Catt$ and $\Catt_{\su}$ for the corresponding categories. Furthermore, we write $\Catt^{\pd}$ and $\Catt^{\pd}_{\su}$ for the full subcategories consisting of only the pasting contexts.

As we have seen, this category contains a collection of objects $\uD^k$ corresponding to the $k$-dimensional disc context. Taken together, these contexts, and their source and target substitutions constitute a *globular* object. $$\begin{tikzpicture}[xscale=2, yscale=.8]
\node (0) at (0,0) {$\cdots\vphantom{D^k}$};
\node (1) at (1,0) {$\uD^{k+1}$};
\node (2) at (2,0) {$\uD^{k}$};
\node (3) at (3,0) {$\cdots\vphantom{D^k}$};
\node (4) at (4,0) {$\uD^0$};
\draw [bend left, ->] (0.north east) to node[above] {$\sigma$} (1.north west);
\draw [bend left, ->] (1.north east) to node[above] {$\sigma$} (2.north west);
\draw [bend left, ->] (2.north east) to node[above] {$\sigma$} (3.north west);
\draw [bend left, ->] (3.north east) to node[above] {$\sigma$} (4.north west);
\draw [bend right, ->] (0.south east) to node[below] {$\tau$} (1.south west);
\draw [bend right, ->] (1.south east) to node[below] {$\tau$} (2.south west);
\draw [bend right, ->] (2.south east) to node[below] {$\tau$} (3.south west);
\draw [bend right, ->] (3.south east) to node[below] {$\tau$} (4.south west);
\end{tikzpicture}$$

A category $\mathcal{C}$ containing a globular object is said to admit *globular limits* if every diagram of the form $$\begin{tikzcd}[row sep=tiny]
      \uD^{i_0} \ar[dr, "\tau^{l_0}"'] & & \uD^{i_2} \ar[dl, "\sigma^{l_2}"] \ar[dr, phantom, "\dots"] & & \uD^{i_n} \ar[dl, "\sigma^{l_n}"] \\
      & \uD^{i_1} & & \uD^{i_{n-1}} &
    \end{tikzcd}$$ admits a limit. Dually, a category $\mathcal{C}$ containing a co-globular object is said to admit *globular sums* if the category $\mathcal{C}^{\op}$ admits globular limits.

The categories $\Catt$ and $\Catt_{\su}$ admit globular limits.

The proof that admits globular limits is to some extent folklore, and has recently been written out [@Benjamin]. The proof for $\Catt_\su$ would be precisely the same, as it only depends on the variable structure of pasting contexts, which is the same in both theories.

With this in hand, we are ready to give our notion of model.

An *$\infty$-category* is a presheaf on the category $\Catt^{\pd}$ which sends globular limits in $\Catt^{\pd}$ to globular sums in $\Set$. A *strictly unital $\infty$-category* is a presheaf on $\Catt^{\pd}_{\su}$ which sends globular limits to globular sums.

In this notion of model of strictly unital $\infty$category, algebraic operations are represented by morphisms of $\Catt_\su^\pd$, and strict unitality of those algebraic operations is then ensured in any model, since any definitionally-equal substitutions are identified in the category.

Reduction
=========

#### Overview

In this section we introduce a reduction relation $\squig$ on types, terms and substitutions, and show that its reflexive, transitive and symmetric closure agrees with definitional equality. We then define a subrelation called *standard reduction*, written $\bsquig$, and show it is a partial function which terminates after finitely many steps, giving us a notion of normal form. Finally, we show that two terms have the same normal form just when they are definitionally equal, meaning that standard reduction gives an algorithm for deciding definitional equality.

#### Convention on Contexts

For this section, and the remainder of the paper, we restrict our attention to contexts $\Gamma$ which are pasting contexts; that is, for which $\Gamma \vdash _p$ is valid. When we speak of a valid type $U$, we mean a type for which there exists a pasting context $\Gamma$ such that $\Gamma \vdash U$ is valid; and when we speak of a valid term $t$, we mean a term for which there is a pasting context $\Gamma$ and type $U$ such that $\Gamma \vdash t :U$ is valid. The reason for this restriction is that it simplifies our analysis—in particular, contexts do not reduce—and it is sufficient for our application to strictly unital $\infty$categories. For valid coherence terms, we freely use Proposition \[uniquecohtype\] to infer information about its structure.

#### Reflexive, Transitive, Symmetric Closures

Given a relation $\squig$, we write $\squig_\r$ for its reflexive closure, $\squig_\t$ for its transitive closure, and $\squig_\s$ for its symmetric closure. When we use multiple such subscripts, we mean this simultaneously; for instance, we write $\squig_\rts$ for its simultaneous reflexive, transitive and symmetric closure.

General reduction
-----------------

We define a reduction relation on types, terms and substitutions, and show that the equivalence relation generated by these relations agrees with definitional equality.

We first define a simple syntactic property on terms, that of being an identity.

\[def:identityterm\] A term is an *identity* if it is of the form $\i_n \sub{\sigma}$ for some $n \in \N$; that is, when its head is an identity coherence.

We emphasise that as a syntactic property, this is not compatible with definitional equality. For example, if $t \equiv \i_n \sub{\sigma}$, then $t$ is an identity; but if we merely have $t = \i_n\sub{\sigma}$, then $t$ is not necessarily an identity.

We now give the reduction relation. The following definitions are given by simultaneous induction. A key point to observe is that determining whether a given type, term or substitution is a redex is a purely *syntactic* condition, which can be mechanically checked, and does not refer to definitional equality.

The basic type $\star$ does not reduce. An arrow type reduces as follows:

1.  if $u \squig u'$, then: $$(u \to _T v) \xsquig {T1} (u' \to_T v)$$

2.  if $v \squig v'$, then: $$(u \to _T v) \xsquig {T2} (v \to _T v')$$

3.  if $T \squig T'$, then: $$(u \to _T v) \xsquig {T3} (u \to _{T'} v)$$

A substitution $\sigma \equiv [ s_1, \ldots, s_n ]$ reduces as follows, given a reduction $s_i^{} \squig s_i'$ of some argument: $$[ s_1, \ldots, s_i, \ldots, s_n ] \xsquig S [ s_1, \ldots, s_i', \ldots, s_n ]$$

\[def:redterms\] Variable terms do not reduce. A coherence term reduces as follows:

1.  if $\sigma \squig \sigma'$, then: $$\begin{aligned}
    \coh (\Gamma : T)[\sigma] &\xsquig A \coh(\Gamma : T)[\sigma']
    \intertext{\item if $t$ is not an identity, and $x \in \var(\Gamma)$ is a locally-maximal variable for which $x[\sigma]$ is an identity, then we define:}
    \coh(\Gamma : T)[\sigma]
    &\xsquig B \coh(\Gamma \dslash x : T\sub{\pi_x})[\sigma \dslash x]
    \intertext{\item[(C)] if $T \squig T'$, then:}
    \coh (\Gamma : T)[\sigma]
    &\xsquig C
    \coh(\Gamma: T')[\sigma]
    \intertext{\item[(D)] the disc removal relation:}
    \coh(\uD^{n+1} : S^n)[\ldots, t]
    &\xsquig D
    t
    \intertext{\item[(E)] if $t$ is not an identity, the endomorphism coherence removal relation (recall the notation $\{T\}$ from Section~\ref{sec:cattsu} of the unfolding of a type $T$):}
    \coh(\Gamma : u \to_T u)[\sigma] &\xsquig E \i_{\dim T+1} \sub{\{T \sub \sigma \}, u \sub{\sigma} }\end{aligned}$$

If we can reduce $u \squig u'$ via some reduction stage (X) above, we say that $u$ is a *general Xredex*, or just an *X-redex*, and we write $u \xsquig X u'$. A given term can be a general X-redex for multiple stages (X). For example, if $u \squig u'$, then the term $\coh (\Gamma : u \to_T u)[\sigma]$ is a C-redex in at least 2 ways, and also an E-redex, as follows: $$\begin{aligned}
\coh(\Gamma : u \to_T u)[\sigma] &\xsquig C \coh(\Gamma : u' \to_T u)[\sigma]
\\
\coh(\Gamma: u \to_T u)[\sigma] &\xsquig C \coh(\Gamma:u \to_T u')[\sigma]
\\
\coh(\Gamma: u \to_T u)[\sigma] &\xsquig E \i_{\dim_T + 1} \sub{ \{ T\sub{\sigma} \}, u \sub{\sigma} }\end{aligned}$$ A term could also have no reductions at all. So reduction is partially defined, and multivalued in general.

We now show that this equivalence relation generated by this reduction relation agrees with definitional equality constructed in Section \[sec:typetheory\]. This is not trivial, because there are some key differences between how these relations are defined. Definitional equality allows pruning with respect to any argument $\alpha\sub\sigma=\i_n \sub \tau$ which is an identity *up to definitional equality*, but the reduction relation $\xsquig B$ only allows pruning with respect to an argument $\alpha \sub \sigma \equiv \i_n \sub \tau$ which is a *syntactic* identity. Definitional equality also allows endo-coherence removal for any $\coh(\Gamma:u \to_T v)[\sigma]$ with $u=v$, while E-reduction requires $u \equiv v$. Furthermore, the reduction relation explicitly proscribes identities as B- or E-redexes, but definitional equality has no such proscription.

\[equalityreduction\] On valid terms, types and substitutions, the equality relation $=$ agrees with $\squig_\rts$.

Clearly $p \squig q$ implies $p = q$, since reduction is by definition a subrelation of equality, so we focus on the converse direction. Also, since the statement for types and substitutions immediately reduces to the statement for terms, we focus on terms here.

We say that a term $p$ is *conservative* if for all terms $q$, we have that $p = q$ implies $p \squig_\rts q$. To prove the lemma, we must therefore show that all terms are conservative. Our proof operates by induction on subterms of $p$, and by case analysis on the equality $p=q$. Almost all such cases are immediate; here we explicitly handle the only nontrivial cases.

For the first nontrivial case, suppose $p=q$ is the following equality, obtained by pruning an identity term: $$\begin{aligned}
&\i_n \ll \ldots, v_2, v^{}_1, v_1', \i_{n-1} \ll \ldots, u_3, u_2, u_1 \rr \rr \\
&= (\coh \uD^{n-1}:\i_{n-1} \to_{(d_{n-1} \to _{S^{n-2}} d_{n-1})} \i_{n-1})[\ldots, v_2, v_1]\end{aligned}$$ By induction on subterms of $p$ we conclude that the terms $u_i$, $v_1'$, $v_i$ are conservative. By validity we must have $u_1 = v_1 = v_1'$ and $u_i \ v_i$, and hence we conclude $u_1 \squig_\rts v_1 \squig_\rts v_1'$ and $u_i \squig_\rts v_i$. We do not have $p \xsquig B q$, since $p$ is an identity term, which are explicitly proscribed as B-redexes. However, $q$ admits an Ereduction, and then a further series of A-reductions obtained by conservativity of the subterms of $p$, as follows: $$\begin{aligned}
q &\xsquig E \i_n \ll \ldots, v_3, v_2, v_1, v_1, \i_{n-1} \ll \ldots, v_3, v_2, v_1 \rr \rr
\\
&\xsquig A _\rts \i_n \ll \ldots, v_3, v_2, v_1^{}, v_1', \i_{n-1} \ll \ldots, u_3, u_2, u_1 \rr \rr
\\&\equiv p\end{aligned}$$ Hence $q \squig_\rts p$ as required.

For the second nontrivial case, suppose $p=q$ is the following equality, by the endo-coherence removal rule: $$p \equiv \coh(\uD^n : d_n \to_{S^{n-1}} d_n)[\ldots, u_2, u_1] = \i_n \ll d_n \ll\ldots, u_2, u_1 \rr, \{ S^{n-1} \ll \ldots, u_2, u_1 \rr \} ] \equiv q$$ We do not have $p \xsquig E q$, since $p$ is an identity term, which is proscribed as an E-redex. However, we note that $$\begin{aligned}
q \equiv \i_n \bigll  d_n \ll \ldots, u_2, u_1 \rr, \{S^{n-1} \ll \ldots, u_2, u_1 \rr \} \bigrr \equiv \i_n \ll \ldots, u_2, u_1 \rr \equiv p\end{aligned}$$ So in fact $p \equiv q$, and hence $p \squig_\rts q$ as required.

For the third nontrivial case, we suppose $p=q$ is the following equality, with $\alpha = \i_n \sub \tau$ an argument in locally-maximal position: $$p \equiv \coh (\Gamma : U)[ \ldots, s, t, \alpha, \ldots ] = \coh (\Gamma \dslash x: U\sub{\pi_x})[ \ldots, s, \ldots ] \equiv q$$ By inductive hypothesis $\alpha$ is conservative, and since $\alpha = \i_n \sub \tau$ that yields the following: $$\begin{aligned}
p \xsquig A _\rts \coh (\Gamma : U)[ \langle \ldots, s, t, \i_n \sub \tau, \ldots \rangle] \xsquig B q\end{aligned}$$ Hence $p \squig_\rts q$ as required.

For the fourth nontrivial case, we suppose $p=q$ is the following equality, where $u=u'$: $$p \equiv \coh (\Gamma : u \to _T u')[\sigma] = \i_{\dim T + 1} \sub{\{T\sub \sigma\}, u \sub \sigma} \equiv q$$ We do not necessarily have $u \equiv u'$, so cannot necessarily conclude $p \xsquig E q$. But by induction on subterms we know $u'$ is conservative, and thus from $u=u'$ we conclude $u' \squig_\rts u$. If $\coh(\Gamma:u \to_T u)$ is the head of an identity term, we proceed as for the second case above. Otherwise we argue as follows: $$\begin{aligned}
p \equiv \coh(\Gamma : u \to _T u')[\sigma] \xsquig C_\rts \coh (\Gamma : u \to _T u)[\sigma] \xsquig E \i_{\dim T + 1} \ll \{ T \sub \sigma \}, u \sub \sigma \rr\end{aligned}$$ This completes the proof.

\[lem:reductionvalidity\] Reduction of types, terms and substitutions preserves validity of judgements:

-   if $\Gamma \vdash A$ is valid and $A \squig A'$, then $\Gamma \vdash A'$ is valid;

-   if $\Gamma \vdash t :A$ is valid and $t \squig t'$, then $\Gamma \vdash t' : A$ is valid;

-   if $\Gamma \vdash t : A$ is valid and $A \squig A'$, then $\Gamma \vdash t : A'$ is valid;

-   if $\Gamma \vdash \sigma : \Delta$ is valid and $\sigma \squig \sigma'$, then $\Gamma \vdash \sigma' : \Delta$ is valid.

Immediate since reduction is a subrelation of definitional equality, and validity can be transported across definitional equality (see Figure \[fig:conversion\].)

Standard reduction
------------------

We now define *standard reduction*, denoted with a bold arrow $\bsquig$, a subrelation of general reduction $\squig$. Standard reduction has the property of being a reduction strategy, in the following sense.

A *reduction strategy* is a relation $\to$ on terms with the property that, if $a \to b$ and $a \to b'$, then $b \equiv b'$.

Put another way, a relation is a reduction strategy just when it is a partial function.

Standard reduction works in a similar way to reduction, but the reductions now have a preference order, so that higher-priority redexes, listed earlier in the following list, block lower-priority redexes listed later. Standard reduction is hence a reduction strategy by construction.

The standard reduction of a type $U \equiv (u \to_T v)$ is given by the first matching reduction in the following list, if any:

1.  if $T \bsquig \widetilde T$, then: $$(u \to _{T\vphantom{\widetilde T}} v) \xbsquig {T0} (u \to _{\widetilde T} v)$$

2.  if $u \bsquig \tilde u$, then: $$(u \to _T v) \xbsquig {T1} (\tilde u \to_T v)$$

3.  if $v \bsquig \tilde v$, then: $$(u \to _T v) \xbsquig {T2} (v \to _T \tilde v)$$

Given a substitution $\sigma \equiv \langle s_1, \ldots, s_n \rangle$, then if $s_i \bsquig \tilde s_i$ is the leftmost argument with a standard reduction, we have the following: $$[ s_1, \ldots, s_i, \ldots, s_n] \xbsquig {S} [ s_1, \ldots, \tilde s_i, \ldots, s_n ]$$

\[standardreductionterms\] A coherence term $t \equiv \coh (\Gamma:U)[\sigma]$ has a *standard reduction* given by the first relation in the following list which is defined, if any:

1.  if $\sigma \bsquig \tilde \sigma$, then: $$\begin{aligned}
    \coh (\Gamma : U)[\sigma] &\xbsquig A \coh(\Gamma : U)[\tilde \sigma]
    \intertext{\item if $t$ is not an identity, and $x \in \var(\Gamma)$ is a locally-maximal variable for which $x[\sigma]$ is an identity, then we define:}
    \coh(\Gamma : U)[\sigma]
    &\xbsquig B \coh(\Gamma \dslash x : U\sub{\pi_x})[\sigma \dslash x]
    \intertext{\item[(C)] if $T \bsquig \tilde T$, then:}
    \coh (\Gamma : T)[\sigma]
    &\xbsquig C
    \coh(\Gamma: \tilde T)[\sigma]
    \intertext{\item[(D)] the disc removal relation:}
    \coh(\uD^{n+1} : S^n)[\ldots, t]
    &\xbsquig D
    t
    \intertext{\item[(E)] if $t$ is not an identity, the endo-coherence removal relation:}
    \coh(\Gamma : u \to_A u)[\sigma] &\xbsquig E \i_{\dim A + 1}  \ll \{A \ll \sigma \rr \}, u \sub{\sigma} \rr\end{aligned}$$

If we can reduce $s \bsquig t$ via some reduction label (X) above, we say that $u$ is a *standard Xredex*. It is an immediate consequence of the definition of standard reduction that it is a reduction strategy; that is, if a term, type or substitution has a standard reduction, it has *exactly one* standard reduction. This is quite unlike general reduction as defined as above. For example, suppose $u \bsquig \tilde u$, and consider the term $t \equiv \coh (\Gamma : u \to_A u)[\sigma]$. It is possible that $t$ is a standard Aredex; failing that, it could be a standard B-redex; failing that, it will certainly be a standard C-redex. Although $t$ is an E-redex (that is, there exists $t'$ with $t \xsquig E t'$), it is [not]{} a *standard* E-redex, since standard C-reductions are higher-priority than standard E-reductions.

Since standard reduction is unique when it exists, it is useful to introduce the following notation.

If $s$ has a standard reduction, we write it as $\tilde s$, and hence $s \bsquig \tilde s$. We call $\tilde s$ the *standard reduct* of $s$.

We now record some results that show a term is reducible just when it is standard reducible.

\[lem:standardtogeneral\] If $s \bsquig \tilde s$, then $s \squig \tilde s$.

By definition, standard reduction is a subrelation of general reduction.

\[lem:generaltostandard\] If $s \squig t$, then there exists a unique $\tilde s$ with $s \bsquig \tilde s$.

Since standard reduction is a reduction strategy, uniqueness is clear. What we must establish is existence. The intuition is straightforward: in essence, we define standard reduction by giving a priority order to the redexes for general reduction, and allowing only the highest-priority redex. The result is then immediate, because if $s$ has at least one reduction, then there must be a highest-priority such reduction.

We prove the result formally as follows, by simultaneous induction on the structure of terms, types, and substitutions. For the base cases, given by the type $\star$ or a variable term, there is no reduction, so the claim is vacuously true.

For a compound type $U\equiv (a\to_T b)$ is a type, then the statement follows immediately by induction on $a$, $b$ or $T$.

For a substitution $\sigma = \langle s_1,\ldots, s_n \rangle$, suppose we have some reduction $\sigma \squig \tau$ arising from some choice of index $i$ and some reduction $s_i \squig t$. Since $\sigma$ has a reducible argument, it must have a leftmost reducible argument, which we can write as $s_j$, with $j \leq i$. By induction on subterms $s_j \bsquig \tilde s_j$, and $[ \ldots, s_{j-1}, s_j, s_{j+1}, \ldots ] \bsquig [ \ldots, s_{j-1}, \tilde s_j, s_{j+1}, \ldots ]$ is the required standard reduction.

For a coherence term $s \equiv \coh (\Gamma : T)[\sigma]$ with a reduction $s \squig t$, we argue by case analysis as follows.

-   If $u$ is an A-redex, there must exist some $\sigma'$ such that $\sigma \leadsto \sigma'$. By induction $\sigma \bsquig \tilde \sigma$, and hence $\coh (\Gamma:T)[\sigma] \xbsquig A \coh(\Gamma:T)[\tilde \sigma]$.

-   If $u$ is not an A-redex, but $u$ is a B-redex, then there must be some leftmost locally-maximal argument of $\Gamma$ with respect to which it is a standard Bredex.

-   If $u$ is not an A- or B-redex, but it is a C-redex, then there must exist some $T'$ such that $T \squig T'$. Hence by induction $T \bsquig \tilde T$, and so $u \xbsquig C \coh (\Gamma : \tilde T)[\sigma]$.

-   If $u$ is not an A-, B- or C-redex, but it is a D-redex, then the D-reduction will be standard.

-   If $u$ is not an A-, B-, C- or D-redex, but it is an E-redex, then the Ereduction will be standard.

-   If $u$ is not an A-, B-, C-, D- or E-redex, then $u$ cannot be reduced, contradicting the hypothesis of the theorem.

This completes the argument.

Termination of standard reduction
---------------------------------

Standard reduction gives us a notion of normal form, as follows.

We define a term, type or substitution to be in *normal form* when it has no reduction, either by standard or general reduction (by Lemmas \[lem:standardtogeneral\] and \[lem:generaltostandard\], these conditions are equivalent.)

In this section we show that standard reduction terminates after finite time on every term, type and substitution. This means that for every term $t$ we can obtain a term $N(t)$ in normal form, by repeatedly applying standard reduction until a normal form is reached.

To work towards our termination result, we consider what happens when we start with a given term and repeatedly perform standard reduction. What we find is a specific pattern of standard reductions, illustrated in Figure \[fig:standardreduction\]. We first perform some family of standard A-reductions. If these terminate, they will be followed by some family of standard B-reductions. If these terminate, they will be followed by some family of standard Creductions. If these terminate, and they are not yet sufficient to yield a normal form, they will be followed either by a single standard D-reduction, giving a term in normal form; or by a single standard E-reduction and a family of standard Areductions, which if they terminate will yield a normal form. We prove this claim as follows.

$$\begin{tikzpicture}
\node (1) at (0,0) {$\bullet$};
\node (2) at (1,0) {$\bullet$};
\node (3) at (2,0) {$\bullet$};
\node (4) at (3,0) {$\bullet$};
\node (5) at (4,1) {$\bullet$};
\node (6) at (5,0) {$\bullet$};
\draw [standard] (1) to node [above] {A} node [below] {\rt} (2);
\draw [standard] (2) to node [above] {B} node [below] {\rt} (3);
\draw [standard] (3) to node [above] {C} node [below] {\rt} (4);
\draw [standard] (4) to [bend right] node [above] {D} node [below] {\r} (6);
\draw [standard] (4) to node [above left=-1pt] {E} node [below right=-2pt] {\r} (5);
\draw [standard] (5) to node [above right=-1pt] {A} node [below left=-2pt] {\rt} (6);
\end{tikzpicture}$$

\[prop:progressive\] The reflexive transitive closure of the standard reduction relation is obtained as the following composite: $$\bsquig_\rt \quad= \quad
\xbsquig {A}_\rt
\,\xbsquig {B}_\rt
\,\xbsquig {C}_\rt
\Big(
\xbsquig {D}_\r
\cup
\,\xbsquig {E}_\r
\,\xbsquig {A}_\rt
\Big)$$

We establish the claim by showing that the following composite reduction pairs and triples are impossible (that is, they are empty as relations).

-   $p \xbsquig B q \xbsquig A r$. For $p$ to be a standard B–redex, it is required that it is not an A-redex, and so the arguments of $p$ must be in normal form. But the arguments of $q$ are a subset of the arguments of $p$, contradicting the claim that $q$ is a standard A-redex.

-   $p \xbsquig C q \xbsquig A r$. For $p$ to be a standard C-redex, it is required that it is not an A-redex, and so the arguments of $p$ must be in normal form. But Creductions do not change the arguments of a term, so the arguments of $q$ are the same as the arguments $p$, contradicting the claim that $q$ is a standard A-redex.

-   $p \xbsquig C q \xbsquig B r$. For $p$ to be a standard C-redex, it is required that it is not a B-redex, a condition that depends on the context and arguments of the term. But C-reductions do not change the context or arguments, so it is impossible that $q$ is a B-redex.

-   $p \xbsquig D q \bsquig r$. For a term to be a standard D-redex, it is required that it is not an A-redex, and so the arguments of $p$ must not be reducible. By the action of D-reduction, the term $q$ is one of the arguments of $p$, contradicting the claim that $q$ is reducible.

-   $p \xbsquig E q \xbsquig B r$. The standard E-reduct $q$ is an identity term, but identity terms are never Bredexes, by definition.

-   $p \xbsquig E q \xbsquig C r$. The standard E-reduct $q$ is an identity term, but identity terms are never Credexes, since the cell part is in normal form.

-   $p \xbsquig E q \xbsquig D r$. The standard E-reduct $q$ is an identity term, but identity terms are never Dredexes, as the head has the wrong syntactic form.

-   $p \xbsquig E q \xbsquig E r$. The standard E-reduct $q$ is an identity term, but identity terms are never Eredexes, by definition.

-   $p \xbsquig E q \xbsquig A_\rt r \xbsquig B s$. The standard E-reduct $q$ is an identity term. Areductions do not change the head, and so $r$ will also be an identity term. But identity terms are never B-redexes, giving a contradiction.

-   $p \xbsquig E q \xbsquig A _\rt r \xbsquig C s$. The standard E-reduct $q$ is an identity term. Areductions do not change the head, and so $r$ will also be an identity term. But identity terms are never C-redexes, giving a contradiction.

-   $p \xbsquig E q \xbsquig A _\rt r \xbsquig D s$. The standard E-reduct $q$ is an identity term. Areductions do not change the head, and so $r$ will also be an identity term. But identity terms are never D-redexes, giving a contradiction.

-   $p \xbsquig E q \xbsquig A _\rt r \xbsquig E s$. The standard E-reduct $q$ is an identity term. Areductions do not change the head, and so $r$ will also be an identity term. But identity terms are never E-redexes, by definition.

The result is then established as follows, by imagining a standard reduction sequence for some given coherence term. Here we refer to composite relations by concatenation; so for example, $t \xbsquig B \xbsquig A t'$ just when there exists some $t''$ with $t \xbsquig B t'' \xbsquig A t'$.

-   Standard A-reductions have the highest priority, so these will be performed first.

-   If the above step terminates, standard B-reductions have the second-highest priority, so we now perform these. Since $\xbsquig B \xbsquig A$ is empty, this will not trigger any additional standard Areductions.

-   If the above step terminates, standard C-reductions have the third-highest priority, so we now perform these. Since $\xbsquig C \xbsquig A$ and $\xbsquig C \xbsquig B$ are both empty, these standard C-reductions will not trigger further standard A- or B-reductions.

-   If the above step terminates, standard D-reductions have the fourth-highest priority. If we can perform a D-reduction, the result will be in normal form, since $\xbsquig D \bsquig$ is empty.

-   If we cannot perform a D-reduction, we consider applying a standard Ereduction, as the standard reduction with fifth-highest priority. If the standard E-reduction cannot be applied, then the term is in normal form, as the standard E-reduction is the last reduction in the list.

-   If the standard E-reduction was successfully applied, it cannot be followed by a standard B-, C-, D-, or E- reduction, since $\xbsquig E \xbsquig B$, $\xbsquig E \xbsquig C$, $\xbsquig E \xbsquig D$ and $\xbsquig E \xbsquig E$ are all shown above to be empty. The only remaining possibility is for the standard E-reduction to be followed by some sequence of standard A-reductions. These Areductions cannot themselves be followed by a standard B-, C-, D- or E-reduction, since we show above that $\xbsquig E \xbsquig A _\rt \xbsquig B$, $\xbsquig E \xbsquig A _\rt \xbsquig C$, $\xbsquig E \xbsquig A _\rt \xbsquig D$ and $\xbsquig E \xbsquig A _\rt \xbsquig E$ are all empty.

This completes the proof.

We next show that standard reduction is terminating.

\[termination\] Standard reduction is terminating on valid types, terms and substitutions.

Standard reduction on types and substitutions is given in terms of standard reduction of a finite family of terms, so we need only check that standard reduction of terms has no infinite sequences. The variable case is trivial, so we consider reduction of some coherence term $t \equiv \coh (\Gamma:T)[\sigma]$.

We proceed by simultaneous induction, on the dimension of $t$, and on subterms of $t$. Since a subterm of a valid term can never have a higher dimension, this is well-defined. The dimension is not defined for variables, but since variables are in normal form, this does not affect the argument.

Thanks to Proposition \[prop:progressive\], we know that the standard reduction of a given term can be separated into finitely many distinct phases of standard A-, B-, C-, D- and E-reduction, with each phase involving standard reductions of a single fixed type. So we need only show that each standard reduction phase will terminate.

-   *Standard A-reduction.* By induction on subterms, since a substitution is of finite length, a given term will have only finitely many standard Areductions.

-   *Standard B-reduction.* Since the context has a finite number of variables, a given term will have only finitely many standard B-reductions.

-   *Standard C-reduction.* Since the cell part of a valid term is formed from terms of strictly lower dimension, it follows by induction on dimension that a term will have only finitely many standard C-reductions.

Standard D- and E-reductions are single-step operations, so no termination argument is necessary for those.

Having now established that standard reduction has no infinite sequences, it is clear every term has a unique normal form with respect to it.

For any term $t$, its *normal form* $N(t)$ is the unique term with $t \bsquig _\rt N(t)$ such that there is no term $u$ with $N(t) \bsquig u$.

For any term $t$, its *distance* is the length, possibly zero, of the unique standard reduction sequence $t \bsquig t_1 \bsquig \cdots \bsquig t_n \bsquig t'$ to its normal form.

Technical results on reduction
------------------------------

Here we collect further results on reduction, mostly of a technical nature, which will be used in the next subsection for our main proof.

\[reductionapplication\] Term substitution is compatible with substitution reduction: $$\sigma \squig \sigma' \quad \Rightarrow \quad u \sub \sigma \squig_{\rt} u \sub {\sigma'}$$

We induct on the structure of $u$. If $u$ is a variable, then either $u\sub \sigma \equiv \sigma' \sub \tau$ or $u\sub \sigma \squig u\sub {\sigma'}$; in either case, we have $u\sub \sigma \squig_{\r} u \sub {\sigma'}$ as required.

Otherwise, we have $u \equiv \coh (\Gamma: U)[\rho]$, and we argue as follows: $$\begin{aligned}
u[\sigma] \equiv{}& \coh (\Gamma : U)[\rho \circ \sigma]
\\
\equiv{}& \coh(\Gamma : U)[ \rho_1 \sub \sigma, \rho_2\sub \sigma, \ldots, \rho_n\sub \sigma ]
\\
\xsquig A _\rt {}& \coh(\Gamma : U)[\rho_1\sub {\sigma'}, \rho_2\sub \sigma, \ldots, \rho_n\sub \sigma ]
\\
\xsquig A _\rt{} & \coh(\Gamma : U)[ \rho_1\sub {\sigma'}, \rho_2\sub {\sigma'}, \ldots, \rho_n\sub {\sigma} ]
\\
\xsquig A _\rt{} & \cdots
\\
\xsquig A _\rt{} & \coh(\Gamma : U)[ \rho_1\sub {\sigma'}, \rho_2\sub {\sigma'}, \ldots, \rho_n\sub {\sigma'} ]
\\
\equiv{}& \coh(\Gamma : U)[\rho \circ \sigma']
\\
\equiv{}& u \sub {\sigma'}\end{aligned}$$ Hence $u\sub{\sigma} \squig_\rt u\sub{\sigma'}$ as required.

If $u$ is a variable, no reduction is possible, in contradiction with hypothesis. We therefore assume $u \equiv \coh (\Gamma : T)[\mu]$ is a coherence term, writing $\mu = [\mu_1, \ldots, \mu_n]$, and proceed by case analysis on the structure of the reduction $u \squig u'$, and by induction on subterms of $u$.

If $u \xsquig A u'$ via some $m_i \squig m_i'$, then we argue as follows: $$\begin{aligned}
u \sub \sigma &\equiv \coh(\Gamma:U)[\mu \circ \sigma]
\\
&\equiv \coh(\Gamma : U)[ \mu_1\sub{\sigma}, \ldots, \mu_i\sub{\sigma}, \ldots, \mu_k\sub{\sigma} ]
\\
& \xsquig A \coh(\Gamma : U)[\mu_1\sub{\sigma}, \ldots, \mu_i'\sub{\sigma}, \ldots, \mu_k\sub{\sigma} ]
\\
& \equiv u \sub {\sigma'}
\intertext{Alternatively, we suppose $u \xsquig B u'$ is the B-reduction $\coh(\Gamma : U)[\mu] \xsquig B \coh(\Gamma \dslash x : U\sub{\pi_x})[\mu \dslash x]$, eliminating some locally-maximal variable $x_i$ of $\Gamma$ for which $x_i \sub \mu \equiv \mu_i$ is an identity. Then $\mu_i\sub{\sigma}$ is also an identity, and hence using Lemma~\ref{lem:quotientsub} we have:}
u \sub \sigma &\equiv \coh (\Gamma : U) [\mu \circ \sigma]
\\
&\equiv\coh (\Gamma : U) [\mu \circ \sigma]
\\
&\xsquig B \coh(\Gamma \dslash x: U \sub {\pi_x} )[(\mu \circ \sigma) \dslash x]
\\
&\equiv \coh (\Gamma \dslash x:U \sub{\pi_x} )[(\mu \dslash x) \circ \sigma]
\\
&\equiv u' \sub \sigma
\intertext{If $u \xsquig C u'$ via some $T \xsquig C T'$, then we argue as follows:}
u \sub\sigma &\equiv \coh(\Gamma : T)[\mu \circ \sigma] \xsquig C \coh (\Gamma : T')[\mu \circ \sigma] \equiv u'\sub{\sigma}
\intertext{If $u \xsquig D u'$ as $\coh (\uD^n:S^{n-1})[\ldots , u'] \xsquig D u'$, then we argue as follows:}
u \sub \sigma &\equiv \coh(\uD^n : S^{n-1})[\ldots, u' \sub\sigma] \xsquig D u' \sub \sigma
\intertext{Finally, if $u \xsquig E u'$ as $\coh (\Gamma:u \to _U u)[\mu] \xsquig E \i_{\dim U+1} \bigll \{U \sub \mu \}, u \sub \mu \bigrr$, then we argue as follows, using Lemma~\ref{lem:typeunfoldingsub}:}
u \sub \sigma &\equiv \coh (\Gamma : u \to_U u)[\mu \circ \sigma]
\\
&\xsquig E \i_{\dim U  + 1} \bigll \{U \ll \mu \circ \sigma \rr \}, u \ll \mu \circ \sigma \rr \bigrr
\\
&\equiv \i_{\dim U + 1} \ll \{U \sub \mu \}, u \sub \mu \bigrr \sub \sigma
\\
&\equiv u' \sub \sigma\end{aligned}$$ This completes the proof.

\[reducelefttermsub\] Term substitution is compatible with term reduction: $$u \squig u' \quad\Rightarrow\quad u\sub{\sigma} \squig u'\sub{\sigma}$$

\[lem:preserveidentities\] If $u$ is an identity, and $u \squig u'$, then $u'$ is an identity.

We recognize an identity term by looking at the head. We prove the result by case analysis on the reduction $u \squig u'$. If $u \xsquig A u'$ the result is immediate, since A-reductions do not change the head. If $u \xsquig B u'$ we have a contradiction, since identity terms cannot be B-redexes by definition. If $u \xsquig C u'$ we again have a contradiction, since a C-reduction acts on the head of the term, but the head of an identity term is in normal form. If $u \xsquig D u'$ we again have a contradiction, since identity terms have the wrong form to be D-redexes. If $u \xsquig E u'$ we again have a contradiction, since identity terms cannot be E-redexes by definition.

\[standardslash\] If $\sigma \bsquig \tilde \sigma$, then $\sigma \dslash x \bsquig_\r \tilde \sigma \dslash x$.

This is immediate, since $\sigma \dslash x$ is a sublist of $\sigma$. If the first reducible argument of $\sigma$ is not in the sublist $\sigma \dslash x$, then $\sigma \dslash x \equiv \tilde \sigma \dslash x$. Otherwise, it will still be the first reducible argument of the sublist, and $\sigma \dslash x \bsquig \tilde \sigma \dslash x$.

\[lem:prunecommute\] Given a context $\Gamma$ and distinct locally-maximal variables $x,y$, and a substitution $\Delta \vdash \sigma : \Gamma$ with $x\sub{\sigma},y\sub{\sigma}$ both identities, the following contexts and substitutions are identical:

\(x) y (y) x & \_x \_y \_y \_x & (x) y (y) x

The first statement is clear from example, in this case showing $(\Gamma \dslash \Omega) \dslash \delta \equiv (\Gamma \dslash \delta) \dslash \Omega$, since the excision operations are independent: $$\tikzset{point/.style={draw, circle, black, fill, inner sep=1.5pt, label={}}}
\begin{aligned}
\begin{tikzpicture}[xscale=.6, scale=.6, font=\scriptsize, every node/.style={inner sep=2pt}]
\draw (0,0) node [point] {} node [left=2pt] {$x$} to node [left] {$f$} node [right] {$y$} (1,1) node [point] {} to node [left] {$g$} node [right] {$\mu$} (2,2) node [point] {} to node [left] {$\nu$} node [right] {$\Omega$} (3,3) node [point] {} to (4,2) node [point] {} to (5,1) node [point] {} to node [left] {$h$} node [right] {$\delta$} (6,2) node [point] {} to (7,1) node [point] {} to (8,0) node [point] {};
\draw [blue] (1.5,2) to +(3,0);
\draw [red] (4.5,1) to +(3,0);

\begin{scope}[xshift=10cm, yshift=3cm]
\draw (0,0) node [point] {} node [left=2pt] {$x$} to node [left] {$f$} node [right] {$y$} (1,1) node [point] {} to node [left] {$g$} node [right] {$\mu$} (2,2) node [point] {} to (3,1) node [point] {} to node [left] {$h$} node [right] {$\delta$} (4,2) node [point] {} to (5,1) node [point] {} to (6,0) node [point] {};
\draw [red] (2.5,1) to +(3,0);
\end{scope}

\begin{scope}[xshift=10cm, yshift=-2cm]
\draw (0,0) node [point] {} node [left=2pt] {$x$} to node [left] {$f$} node [right] {$y$} (1,1) node [point] {} to node [left] {$g$} node [right] {$\mu$} (2,2) node [point] {} to node [left] {$\nu$} node [right] {$\Omega$} (3,3) node [point] {} to (4,2) node [point] {} to (5,1) node [point] {} to (6,0) node [point] {};
\draw [blue] (1.5,2) to +(3,0);
\end{scope}

\begin{scope}[xshift=18cm, yshift=0cm]
\draw (0,0) node [point] {} node [left=2pt] {$x$} to node [left] {$f$} node [right] {$y$} (1,1) node [point] {} to node [left] {$g$} node [right] {$\mu$} (2,2) node [point] {} to (3,1) node [point] {} to (4,0) node [point] {};
\end{scope}

\node [red, rotate=-30] at (9.5,0) {$\squig$};
\node [blue, rotate=30] at (8,2.5) {$\squig$};
\node [blue, rotate=30] at (16,0) {$\squig$};
\node [red, rotate=-30] at (18,2.5) {$\squig$};

\end{tikzpicture}
\end{aligned}$$ The other claims follows similarly.

\[lem:discsubtrick\] For a valid substitution $\Delta \vdash \sigma : \uD^n$, we have for all $i \leq n$: $$\begin{aligned}
d_i \sub \sigma &= \src^{n-i}(d_n \sub \sigma)
&
d'_i \sub \sigma &= \tgt^{n-i}(d_n \sub \sigma)\end{aligned}$$

Extending the substitution construction rule along definitional equality we must have $\src(d_n \sub \sigma) = \src(d_n) \sub \sigma$, and similarly for $\tgt$. The result follows.

\[lem:prunefactorization\] For a valid substitution $\sigma$ that sends a locally-maximal variable $x$ to an identity, we have $\pi_x \circ (\sigma \dslash x) = \sigma$.

Suppose $x[\sigma] = \i_n \sub {\tau_0^{}, \tau'_0, \ldots, \tau^{}_{n-1}, \tau'_{n-1}, \tau^{}_n}$, an identity, and suppose $\src(x) = v$ and $\tgt(x)=w$ as variables. Then by the substitution construction rule transported along definitional equality, $\src(\i_n \sub \tau) = \tgt(\i_n \sub \tau) = \tau_n$. So $\sigma = [ \ldots, \tau_n, \tau_n, \i_n \sub \tau, \ldots]$, and furthermore $\sigma \dslash x = [\ldots, \tau_n, \ldots]$, and $\pi_x \equiv [\ldots, v, v, \i_n \sub {\src^n(v), \tgt^n(v), \ldots, \src(v), \tgt(v), v}, \ldots]$. Composing, we obtain: $$\begin{aligned}
\pi_x \circ (\sigma \dslash x) &\equiv [ \ldots, v \ll \sigma \dslash x \rr, v \ll \sigma \dslash x \rr,
\\&\qquad\i_n \ll \src^n(v), \tgt^n(v),  \ldots, \src(v), \tgt(v),  v  \rr \ll \sigma \dslash x \rr, \ldots]
\\
&= [ \ldots, \tau_n, \tau_n, \i_n \ll \src^n(\tau_n), \tgt^n(\tau_n)\ldots, \src(\tau_n), \tgt(\tau_n),\tau_n \rr , \ldots ]
\\
&= [ \ldots, \tau_n, \tau_n, \i_n \ll \tau_0^{}, \tau'_0, \ldots, \tau_{n-1}^{}, \tau'_{n-1}, \tau_n^{} \rr , \ldots ]
\\
& = \sigma\end{aligned}$$ The penultimate step here uses Lemma \[lem:discsubtrick\]. This completes the proof.

Standard reduction generates definitional equality
--------------------------------------------------

We show that the symmetric, transitive and reflexive closure of standard reduction generates definitional equality. Since we have already shown that standard reduction is a terminating reduction strategy, this gives an algorithm to determine whether two given terms are definitionally equal, by computing their standard normal forms and checking if they are syntactically equal.

\[close\_rts\] If $a \bsquig_\rts b$, there exists $c$ with $a \bsquig_\rt c$ and $b \bsquig_\rt c$.

This is immediate, since $\bsquig$ is a reduction strategy.

\[standardise\] We have the following, for any valid term $s$:

1.  If $s \squig t$, we can find terms $a, b$ which admit a reduction $a \squig_\r b$ and standard reductions $s \bsquig_\t a$, $t \bsquig_\rts b$, illustrated as follows: $$\begin{tikzpicture}[xscale=1.2, yscale=1.06]
    \node (s) at (0,0) {$s$};
    \node (t) at (1,0) {$t$};
    \node (a) at (0,-1) {$a$};
    \node (b) at (1,-1) {$b$};
    \draw [nonstandard] (s) to (t);
    \draw [nonstandard] (a) to node [below] {\r} (b);
    \draw [standard] (s) to node [left] {\t} (a);
    \draw [standard] (t) to node [right] {\rts} (b);
    \end{tikzpicture}$$

2.  If $s = t$, then $s \bsquig_\rts t$.

Since by Proposition \[termination\] every term reaches normal form after a finite number of standard reductions, and since by Lemma \[equalityreduction\] reduction generates equality, it is clear that statement (i) implies statement (ii). We therefore focus here on the proof of (i).

We can neglect the case of $s$ being a variable, since variables do not reduce. It follows that $s$ is a coherence term, and since the dimension of a valid coherence term is well-defined, we will make use of that throughout. The proof of (i) is by simultaneous induction on the dimension of $s$, and on subterms of $s$. Since no subterm of $s$ has a greater dimension than $s$ itself, this is consistent.

One possibility, which arises several times in the case analysis below, is that the reduction $s \squig t$ is itself standard (that is, $t \equiv \tilde s$.) We can handle this case once-and-for-all as follows: $$\label{alreadystandard}
\begin{aligned}
\begin{tikzpicture}[xscale=1.2, yscale=1.06]
\node (s) at (0,0) {$s$};
\node (t) at (1,0) {$t$};
\node (a) at (0,-1) {$\tilde s$};
\node (b) at (1,-1) {$\tilde s$};
\draw [nonstandard] (s) to (t);
\draw [triple] (a) to node [below] {} (b);
\draw [standard] (s) to node [left] {} (a);
\draw [triple] (t) to node [right] {} (b);
\end{tikzpicture}
\end{aligned}$$ We refer to this argument below where it is needed.

We now begin the main proof of property (i), by case analysis on the reduction $s \squig t$.

*First case $s \xsquig {A} t$.* We suppose $s \equiv \coh (\Gamma : T)[\sigma]$, and that $s \xsquig A t$ by reducing an argument of $\sigma$ via $s_i^{} \squig s_i'$. Then $s$ must be a standard A-redex, because if some argument is not in normal form, there must exist a leftmost argument not in normal form; so we have $s \xbsquig A \tilde s$.

Suppose $s \xsquig A t$ and $s \xbsquig A \tilde s$ act by reducing the same argument of $s_i$ of $\sigma$, via $s_i \squig s_i'$ and $s_i \bsquig \tilde s_i$ respectively. If $s'_i \equiv \tilde s_i^{}$ then we are done by the argument above expression  above. Otherwise the result holds by induction on the subterm $s_i$, as follows: $$\begin{tikzpicture}[xscale=4.5, yscale=1.2]
\node (tl) at (0,0) {$\coh (\Gamma : T)[ \ldots, s_i, \ldots ]$};
\node (tr) at (1,0) {$\coh (\Gamma : T)[ \ldots, s_i', \ldots ]$};
\node (bl) at (0,-1) {$\coh (\Gamma : T)[ \ldots, \tilde s_i, \ldots ]$};
\node (br) at (1,-1) {$\coh (\Gamma : T)[ \ldots, q, \ldots ]$};
\draw [nonstandard] (tl) to node [above] {A} (tr);
\draw [standard] (tl) to node [left] {A} (bl);
\draw [standard] (tr) to node [left] {\rts} node [right] {A} (br);
\draw [nonstandard] (bl) to node [below] {A} (br);
\end{tikzpicture}$$ Alternatively, suppose they act by reducing different arguments of $\sigma$. Then the redexes are independent, and we argue as follows: $$\begin{tikzpicture}[xscale=5.5, yscale=1.2]
\node (tl) at (0,0) {$\coh (\Gamma : T)[ \ldots, s_i, \ldots, s_j, \ldots ]$};
\node (tr) at (1,0) {$\coh (\Gamma : T)[ \ldots, s_i^{}, \ldots, s_j', \ldots ]$};
\node (bl) at (0,-1) {$\coh (\Gamma : T)[ \ldots, \tilde s_i, \ldots, s_j, \ldots]$};
\node (br) at (1,-1) {$\coh (\Gamma : T)[ \ldots, \tilde s^{}_i, \ldots, s_j', \ldots]$};
\draw [nonstandard] (tl) to node [above] {A} (tr);
\draw [standard] (tl) to node [left] {A} (bl);
\draw [standard] (tr) to node [left] {} node [right] {A} (br);
\draw [nonstandard] (bl) to node [below] {A} (br);
\end{tikzpicture}$$

*Second case $s \xsquig {B} t$.* For this case, we suppose $s \xsquig{B} t$ as follows: $$s \equiv \coh (\Gamma: T)[\sigma] \xsquig B \coh (\Gamma \dslash x: T \sub{\pi_x} )[\sigma \dslash x] \equiv t$$ We proceed by case analysis on the standard reduction $s \bsquig \tilde s$.

*Standard A-reduction.* In this case, we argue as follows: $$\begin{tikzpicture}[xscale=4, yscale=1.2]
\node (tl) at (0,0) {$\coh (\Gamma: T)[\sigma]$};
\node (tr) at (1,0) {$\coh (\Gamma \dslash x: T \sub{\pi_x})[\sigma \dslash x]$};
\node (bl) at (0,-1) {$\coh (\Gamma : T)[\tilde \sigma]$};
\node (br) at (1,-1) {$\coh (\Gamma \dslash x: T \sub{\pi_x})[\tilde \sigma \dslash x]$};
\draw [nonstandard] (tl) to node [above] {B} (tr);
\draw [standard] (tl) to node [left] {A} node [right] {} (bl);
\draw [standard] (tr) to node [right] {A} (br);
\draw [nonstandard] (bl) to node [below] {B} (br);
\end{tikzpicture}$$ Since the upper B-reduction is valid, we know that $x\sub{\sigma}$ is an identity; then by Lemma \[lem:preserveidentities\] we also have that $x\sub{\tilde \sigma}$ is an identity, and so the lower B-reduction is valid. Validity of the standard A-reduction on the right of the square follows from Lemma \[standardslash\].

*Standard B-reduction.* We suppose $s$ is a standard B-redex with respect to some locally-maximal variable $y$. If $x \equiv y$, then the reductions are the same, and this case is handled by the general argument above expression . Otherwise, we argue as follows, using Lemma \[lem:prunecommute\]: $$\begin{tikzpicture}[xscale=6, yscale=1.2]
\node (tl) at (0,0) {$\coh (\Gamma: T)[\sigma]$};
\node (tr) at (1,0) {$\coh (\Gamma \dslash x: T \sub{\pi_x})[\sigma \dslash x]$};
\node (bl) at (0,-2) {$\coh (\Gamma \dslash y: T \sub{\pi_y})[\sigma \dslash y]$};
\node (br) at (1,-2) {$\coh \big((\Gamma \sslash y) \sslash x : T \sub{\pi_y} \sub{\pi_x} \big)[(\sigma \sslash y) \sslash x]$};
\node (rr) at (1,-1) {$\coh \big((\Gamma \sslash x) \sslash y : T \sub{\pi_x} \sub{\pi_y} \big) [(\sigma \sslash x) \sslash y]$};
\draw [nonstandard] (tl) to node [above] {B} (tr);
\draw [standard] (tl) to node [left] {B} node [right] {} (bl);
\draw [standard] (tr) to node [right] {B} (rr);
\draw [nonstandard] (bl) to node [below] {B} (br);
\draw [triple] (rr) to (br);
\end{tikzpicture}$$

*Third case $s \xsquig {C} t$.* Suppose $s \equiv \coh (\Gamma : T)[\sigma]$, and $s \xsquig{C} t$ acts via some type reduction $T \squig U$. Then we argue by case analysis on the reduction $s \bsquig \tilde s$.

*Standard A-reduction.* In this case we have the following: $$\begin{tikzpicture}[xscale=4, yscale=1.2]
\node (tl) at (0,0) {$\coh (\Gamma: T)[\sigma]$};
\node (tr) at (1,0) {$\coh (\Gamma: U)[\sigma]$};
\node (bl) at (0,-1) {$\coh (\Gamma : T)[\tilde \sigma]$};
\node (br) at (1,-1) {$\coh (\Gamma: U)[\tilde \sigma]$};
\draw [nonstandard] (tl) to node [above] {C} (tr);
\draw [standard] (tl) to node [left] {A} (bl);
\draw [standard] (tr) to node [right] {A} (br);
\draw [nonstandard] (bl) to node [below] {C} (br);
\end{tikzpicture}$$

*Standard B-reduction.* If $s$ is a standard B-redex, we have the following, employing Lemma \[reducelefttermsub\]: $$\begin{tikzpicture}[xscale=6, yscale=1.2]
\node (tl) at (0,0) {$\coh (\Gamma: T)[\sigma]$};
\node (tr) at (1,0) {$\coh (\Gamma: U)[\sigma]$};
\node (bl) at (0,-1) {$\coh (\Gamma \dslash x : T \sub{\pi_x})[ \sigma \dslash x ]$};
\node (br) at (1,-1) {$\coh (\Gamma \dslash x: U \sub{\pi_x} )[\sigma \dslash x]$};
\draw [nonstandard] (tl) to node [above] {C} (tr);
\draw [standard] (tl) to node [left] {B} (bl);
\draw [standard] (tr) to node [right] {B} (br);
\draw [nonstandard] (bl) to node [below] {C} (br);
\end{tikzpicture}$$

*Standard C-reduction.* Suppose $s$ is a standard C-redex via a standard type reduction $T \bsquig \tilde T$. If $\tilde T \equiv U$, we are done by the argument above expression . Otherwise, since $T \squig U$, by induction on subterms we know that $U \bsquig_\rts T$, and we argue as follows: $$\begin{tikzpicture}[xscale=4, yscale=2]
\node (tl) at (0,0) {$\coh (\Gamma: T)[\sigma]$};
\node (tr) at (1,0) {$\coh (\Gamma: U)[\sigma]$};
\node (bl) at (0,-1) {$\coh (\Gamma : \tilde T)[ \tau ]$};
\node (br) at (1,-1) {$\coh (\Gamma: \tilde T)[\tau]$};
\node (brr) at (1,-.5) {$\coh (\Gamma: T)[\tau]$};
\draw [nonstandard] (tl) to node [above] {C} (tr);
\draw [standard] (tl) to node [left] {C} node [right] {\t} (bl);
\draw [standard] (tr) to node [right] {C} node [left] {\rts} (brr);
\draw [standard] (brr) to node [right] {C} (br);
\draw [triple] (bl) to node [below] {} (br);
\end{tikzpicture}$$

*Fourth case $s \stackrel {\mathrm{D}} \squig t$.* We suppose $s \stackrel {\mathrm{D}} \squig t$ as follows: $$s \equiv \coh (\uD^{n+1}: S^n)[ \ldots, t] \xsquig D t$$ Then we consider the standard reduction for $s$.

*Standard A-reduction.* Supposing $t \bsquig \tilde t$ is the leftmost reducible argument of $s$, then we have the following: $$\begin{tikzpicture}[xscale=4, yscale=1.2]
\node (tl) at (0,0) {$\coh (\uD^{n+1}: S^n)[ \ldots, t ]$};
\node (tr) at (1,0) {$t$};
\node (bl) at (0,-1) {$\coh (\uD^{n+1}: S^n)[ \ldots, \tilde t]$};
\node (br) at (1,-1) {$\tilde t$};
\draw [nonstandard] (tl) to node [above] {D} (tr);
\draw [standard] (tl) to node [left] {A} (bl);
\draw [standard] (tr) to node [left] {} (br);
\draw [nonstandard] (bl) to node [below] {D} (br);
\end{tikzpicture}$$ Otherwise, let $p$ be the leftmost reducible argument of $s$. Then we argue as follows: $$\begin{tikzpicture}[xscale=4.5, yscale=1.2]
\node (tl) at (0,0) {$\coh (\uD^{n+1}: S^n)[ \ldots, p, \ldots, t]$};
\node (tr) at (1,0) {$p$};
\node (bl) at (0,-1) {$\coh (\uD^{n+1}: S^n)[ \ldots, \tilde p, \ldots, t]$};
\node (br) at (1,-1) {$p$};
\draw [nonstandard] (tl) to node [above] {D} (tr);
\draw [standard] (tl) to node [left] {A} (bl);
\draw [triple] (tr) to node [left] {} (br);
\draw [nonstandard] (bl) to node [below] {D} (br);
\end{tikzpicture}$$

*Standard B-reduction.* In this case we must have $t \equiv \i_n \ll \ldots, q_2, q_1 \rr$, and hence $s \equiv \coh (\uD^{n+1}: S^n)[\ldots, p_2^{}, p_1^{}, p_1', \i_n \ll \ldots, q_2, q_1 \rr ]$. Since $s$ is valid we deduce $q_1^{} = p_1^{} = p'_1$ and $q_i = p_i$. It follows by induction on subterms that $q_i \bsquig_\rts p_i$. We put this together as follows: $$\begin{tikzpicture}[xscale=6, yscale=1.2]
\node (tl) at (0,0) {$\coh (\uD^{n+1}: S^n)[\ldots, p_2^{}, p_1^{}, p_1', \i_n \ll \ldots, q_2, q_1 \rr ]$};
\node (tr) at (1,0) {$\i_n \ll \ldots, q_2, q_1 \rr$};
\node (bl) at (0,-1) {$\coh (\uD^{n}: d_n \to_{S^{n-1}} d_n)[ \ldots, p_2, p_1 ]$};
\node (br) at (1,-1) {$\i_n \ll \ldots, p_2, p_1 \rr$};
\draw [nonstandard] (tl) to node [above] {D} (tr);
\draw [standard] (tl) to node [left] {B} (bl);
\draw [standard] (tr) to node [right] {A} node [left] {\rts} (br);
\draw [triple] (bl) to (br);
\end{tikzpicture}$$

The term $s$ cannot be C-redex, since the type $S^n$ is in normal form, being constructed entirely from variables.

In this case, the result follows from the argument around around expression  above.

*Fifth case $s \stackrel {\mathrm{E}} \squig t$.* We suppose $s \stackrel {\mathrm{E}} \squig t$ as follows, for $n = \dim T + 1$: $$s \equiv \coh (\Gamma: u \to_T u)[\sigma] \squig \i_{n} \ll \{ T \sub \sigma \}, u \sub \sigma \rr \equiv t$$ We now consider the structure of the standard reduction $s \bsquig \tilde s$.

*Standard A-reduction.* If $\sigma \bsquig \tilde \sigma$ then by Lemma \[reductionapplication\] we have $u \sub \sigma \squig_\rt u\ll \tilde \sigma \rr$ and $T \sub \sigma \squig_\rt T \sub{\tilde \sigma}$. We conclude by induction on dimension that $\i_{n} \ll \{ T \sub \sigma \}, u \sub \sigma \rr \xbsquig A _\rts \i_{n} \ll \{ T \sub {\tilde \sigma} \}, u \sub {\tilde \sigma} \rr$. Altogether, we have the following as required: $$\begin{tikzpicture}[xscale=4, yscale=1.2]
\node (tl) at (0,0) {$\coh (\Gamma : u \to_T u)[ \sigma]$};
\node (tr) at (1,0) {$\i_{n} \ll \{ T \sub \sigma \}, u \sub \sigma \rr$};
\node (bl) at (0,-1) {$\coh (\Gamma : u \to_T u)[\tilde \sigma]$};
\node (br) at (1,-1) {$\i_{n} \ll \{ T \sub {\tilde \sigma} \}, u \sub {\tilde \sigma} \rr$};
\draw [nonstandard] (tl) to node [above] {E} (tr);
\draw [standard] (tl) to node [left] {A} (bl);
\draw [standard] (tr) to node [left] {\rts} node [right] {A} (br);
\draw [nonstandard] (bl) to node [below] {E} (br);
\end{tikzpicture}$$

*Standard B-reduction.* In this case we have the following: $$\begin{tikzpicture}[xscale=6, yscale=1.2]
\node (tl) at (0,0) {$\coh (\Gamma : u \to_T u)[ \sigma]$};
\node (tr) at (1,0) {$\i_{n} \bigll \{ T \sub \sigma \}, u \sub \sigma \bigrr$};
\node (bl) at (0,-1) {$\coh (\Gamma \dslash x: u \sub{\pi_x} \to_{T \sub{\pi_x}} u \sub{\pi_x})[\sigma \dslash x]$};
\node (br) at (1,-1) {$\i_n \bigll \{ T\sub{\pi_x} \sub{\sigma \dslash x} \}, u \sub{\pi_x} \sub{\sigma \dslash x} \bigrr$};
\draw [nonstandard] (tl) to node [above] {E} (tr);
\draw [standard] (tl) to node [left] {B} (bl);
\draw [standard] (tr) to node [left] {$\rts$} node [right] {A} (br);
\draw [nonstandard] (bl) to node [below] {E} (br);
\end{tikzpicture}$$ We obtain the right-hand standard A-reduction as follows. From Lemma \[lem:prunefactorization\] we know $\sigma = \pi_x \circ (\sigma \dslash x)$, and hence $u \sub \sigma = u \sub{\pi_x} \sub{\sigma \dslash x}$ and $T \sub\sigma = T \sub {\pi_x} \sub{\sigma \dslash x}$. By induction we conclude $u \sub\sigma \bsquig_\rts u \sub{\pi_x} \sub{\sigma \dslash x}$ and $T \sub \sigma \bsquig_\rts T \sub{\pi_x} \sub{\sigma \dslash x}$.

*Standard C-reduction.* Since $u \sub \sigma = u' \sub \sigma$ and $T \sub\sigma = T' \sub\sigma$, it follows by induction that $u \sub\sigma \bsquig_\rts u' \sub\sigma$ and $T \sub\sigma \bsquig_\rts T' \sub\sigma$, and hence that $\i_{n} \ll \{ T \sub \sigma \}, u \sub \sigma \rr \xbsquig A  _\rts \i_{n} \ll \{ T' \sub \sigma \}, u' \sub \sigma \rr$. We then have the following: $$\begin{tikzpicture}[xscale=6, yscale=1.2]
\node (tl) at (0,0) {$\coh (\Gamma : u \to_T u)[ \sigma]$};
\node (tr) at (1,0) {$\i_{n} \ll \{ T \sub \sigma \}, u \sub \sigma \rr$};
\node (br) at (1,-1) {$\i_{n} \ll \{N( T) \sub \sigma \}, N(u) \sub \sigma \rr$};
\node (bbbl) at (0,-1) {$\coh (\Gamma : N(u) \to_{N(T)} N(u))[\sigma]$};
\draw [nonstandard] (tl) to node [above] {E} (tr);
\draw [standard] (tr) to node [left] {\rts} node [right] {A} (br);
\draw [nonstandard] (bbbl) to node [below] {E} (br);
\draw [standard] (tl) to node [left] {C} node [right] {\t} (bbbl);
\end{tikzpicture}$$

*Standard D-reduction.* The term $s$ cannot be a D-redex, as the term $s$ has an incompatible structure.

*Standard E-reduction.* In this case we are done, with the result following from the argument around around expression .

This completes the argument.

\[cor:decidedefeq\] We have $s = t$ if and only if $N(s) \equiv N(t)$.

Examples
--------

Now that we can decide definitional equality, we can investigate some examples. These will illustrate the theory, and in particular allow us to show it is non-trivial (that is, there is not a single definitional equality class of terms.) To begin with, consider the context describing the three composable 1-morphisms: $$\Gamma = (x : \star)(y : \star)(f : x \to_\star y) (z : \star)(g : y \to_\star z)(w : \star)(h : z \to_\star w)$$ Then the following three terms are all in normal form, but distinct, demonstrating the non-triviality of the theory:

-   $\mathsf{comp_3} \ll x,y,f,z,g,w,h \rr$, which represents $f \cdot g \cdot h$, the unbiased 3-fold composite;

-   $\mathsf{comp_2} \ll x, z, \mathsf{comp_2} \ll x, y, f,z, g \rr ,w, h \rr$, which represents $(f \cdot g) \cdot h$, a biased binary composite;

-   $\mathsf{comp_2} \ll x, y, f,w, \mathsf{comp_2} \ll y, z, g,w, h \rr \rr$, which represents $f \cdot (g \cdot h)$, another biased binary composite.

To see the reductions of the theory working, let us first normalize the following term, showing that $f \cdot \i_y$ normalizes to $f$: $$\begin{aligned}
\mathsf{comp_2}\sub{x,y,f,y,\i_0\sub{y}} \xbsquig B
\mathsf{comp_1}\sub{x,y,f}
\xbsquig D 
f\end{aligned}$$ This is one of the examples we considered in Section 2; here we see that our standard reduction relation can algorithmically extract the normal form. For our second example, we show that $\lambda_f : f \cdot \i_y \Rightarrow f$ normalizes to $\id_f$: $$\begin{aligned}
\mathsf{unit\mhyphen r} &\equiv \coh((x : \star)(y : \star)(f : x \to_\star y) : \mathsf{comp_2}\sub{x,y,f,y,\i_0\sub{y}} \to_{x \to_\star y} f)[x,y,f]
\\*
&\xbsquig {C} \coh((x : \star)(y : \star)(f : x \to_\star y) : \mathsf{comp_1}\sub{x,y,f} \to_{x \to_\star y} f)[x,y,f]
\\*
&\xbsquig C
\coh((x : \star)(y : \star)(f : x \to_\star y) : f \to_{x \to_\star y} f)[x,y,f]
\\*
&\equiv \i_1 \sub{x, y, f}\end{aligned}$$ These examples illustrate the way that standard reduction lets us find the strictly unital normal form for any $\infty$categorical operation, expressed as a $\Catt_\su$ term.

Disc trivialization
===================

In the following section, we prove a structure theorem that says in a disc context $\uD^n$, up to definitional equality, every term is either a variable, or an iterated identity on a variable. So if we restrict to terms that use *all* variables of $\uD^n$ (that is, the terms which do not factor through a smaller context), then there is exactly one definitional equivalence class of term in each dimension $k \geq n$, the normal form of which is the locally-maximal variable $d_n$ or an iterated identity on this. In this sense, $\Catt_\su$ trivializes disc contexts.

This provides an interesting point of comparison with work of Batanin, Cisinski and Weber [@Batanin2013], discussed further in Section \[sec:relatedwork\], where strictly unital weak $\infty$categories are defined as algebras over a certain operad, defined to be the universal one which trivializes the operations over discs, and which satisfies a unit compatibility property. By showing our theory also trivializes operations over discs, we claim that in this respect, our theory is at least as strict.

#### Preparatory Lemmas

Before we can prove the main theorem of this section, we need to establish some technical results about pasting contexts.

We say that a substitution $\Delta \vdash \sigma : \Gamma$ is a *variable-to-variable substitution* if for all $x \in \var(\Gamma)$, we have that $x \sub \sigma$ is again a variable.

\[lem:variablestovariables\] Let $\uD^n\vdash \sigma: \Gamma $ be a valid substitution which is in normal form, and which sends locally-maximal variables of $\Gamma$ to variables of $\uD^n$. Then $\sigma$ is a variable-to-variable substitution.

Let $v$ be a variable of $\Gamma$. Then there is some locally-maximal variable $w$ of $\Gamma$ such that $v = \src^k(w)$ for some $k \in \N$. It follows from the formation rules for substitution that $\src^k(w \sub \sigma) = \src^k(w) \sub \sigma \equiv v \sub \sigma$. Since we are given that $w \sub \sigma$ is a variable, it follows that $v \sub \sigma$ is a variable up to definitional equivalence. But since $\sigma$ is normalized, $v \sub \sigma$ must be precisely a variable.

For every $k<n$, there are two variable-to-variable substitutions , which map the $k$disc context into the appropriate source or target context of $\uD^n$. We also have $\uD^n \vdash \id_{\uD^n} : \uD^n$, the identity substitution. We call these *subdisc inclusions.* We now show that every valid variable-to-variable substitution is of this form.

\[lem:pastingfact\] Let $\uD^n \vdash \sigma:\Gamma$ be a valid variable-to-variable substitution. Then we have $\Gamma \equiv \uD^k$ for some $k \leq n$, and $\sigma$ is a subdisc inclusion.

The variables of a pasting context $\Gamma$ form a globular set $\g(\Gamma)$ in an obvious way, and the substitution well-typedness condition means that a variable-to-variable substitution $\uD^n \vdash \sigma : \Gamma$ induces a function of globular sets $\sigma : \g(\Gamma) \to \g(\uD^n)$. Suppose for a contradiction $\Gamma$ is *not* a disc: then it must contain some sub–Dyck word $(\Uparrow (\Downarrow (\Uparrow (\cdots )\,y\,f)\cdots ) z\,g \cdots)$, and we have $\tgt(f) = \src(g)$. Then also $\tgt(\sigma(f)) = \src(\sigma(g))$; but now we have a contradiction, since the globular set of a disc does not have any pair of elements related in this way.

We conclude that $\Gamma \equiv \uD^k$ for some $k \leq n$. It remains to show that $\sigma$ is a subdisc inclusion. For this, suppose $k=n$. Then since $\sigma$ preserves variable dimension, we must have $d_n \sub \sigma = d_n$, and this extends uniquely to the other variables, since $\sigma$ is a function of globular sets, and we conclude $\sigma \equiv \id_{\uD^n}$. Otherwise, suppose $k < n$. Then we can choose $d_k \sub \sigma = d_k$ or $d_k \sub \sigma = d'_k$, and once again, both extend uniquely, yielding $\sigma \equiv \partial _{k,n}^-$ and $\sigma \equiv \partial _{k,n}^+$ respectively.

Given a valid term $t$ in some context $\Gamma$, its *canonical identity* is $\i(t) := \i_{\dim(t)} \ll \{\ty(t)\}, t \rr$. Canonical identities can be distinguished from ordinary identities $\i_n \sub \sigma$ because we do not need to give the dimension subscript, as it can be inferred from the term and the supplied context; because we use round brackets; and because we supply a term as an argument, rather than a substitution. A term is an *iterated canonical identity* if it is of the form $\i^k(t)$, by applying this construction $k$ times for $k > 0$. We now show that if a term is definitionally equal to an ordinary identity $\i_n \sub \sigma$, it is definitionally equal to a canonical identity.

\[lem:canonicalid\] If $t$ is a valid term of $\Gamma$ with $t = \i_n \sub {\ldots , p}$, then $t = \i(p)$.

We define $\sigma := [\ldots , p_2^{}, p_2', p_1^{}, p'_1, p]$. Because $\Gamma \vdash \sigma : \uD^n$ is a valid substitution, it must satisfy the substitution typing conditions up to definitional equality, so we conclude for each $0 < k \leq n$ the following: $$\begin{aligned}
p_k \equiv d_{n-k} \sub \sigma \equiv \src^k(d_n) \sub \sigma = \src^k(d_n \sub \sigma) \equiv \src^k(p)
\\
p'_k \equiv d'_{n-k} \sub \sigma \equiv \tgt^k(d_n) \sub \sigma = \tgt^k(d_n \sub \sigma) \equiv \tgt ^k (p)\end{aligned}$$ We now reason as follows: $$\begin{aligned}
t &\equiv \i_n \ll \ldots,  p_2, p_2', p_1, p_1', p \rr
\\
& = \i_n \ll \ldots, \src^2(p), \tgt^2(p), \src(p), \tgt(p),p \rr
\\
& \equiv \i(p) \end{aligned}$$ This completes the proof.

#### Structure Theorem

We are now prepared to prove our structure theorem characterizing definitional equality for valid terms over discs, which says that any term of $\uD^n$ in normal form must be syntactically equal to $\i^k(d)$ for some $k \in \N$ and some variable $d$ of $\uD^n$.

\[thm:disctrivialization\] Suppose $t$ is valid in $\uD^n$. Then $t$ is definitionally equal to a variable, or to the iterated canonical identity on a variable.

If $t$ is a variable, we are done. Otherwise, $t$ is a coherence term, and we have that . By Corollary \[cor:decidedefeq\], we may assume without loss of generality that $t$ is in normal form.

If $t$ is an identity, then by Lemma \[lem:canonicalid\] we know $t = \i(u)$. By induction on dimension, $u$ is therefore either a variable or a iterated identity on a variable, and we are done.

It remains to consider the case that $t\equiv \coh(\Gamma:U)[\sigma]$ is not an identity. We will see that we are now guaranteed to obtain a contradiction. Since $t$ is in normal form, we know that $t$ is not an A-, B-, C-, D- or E-redex, and we use these facts freely below.

First, note that $\uD^n \vdash \sigma:\Gamma$ maps locally maximal variables of $\Gamma$ to non-identity terms of $\uD^n$ (or else $t$ would be a B-redex), and these terms are in normal form (or else $t$ would be an Aredex). Hence, by induction on subterms, we may assume that $\sigma$ maps locally-maximal variables to variables. By Lemma \[lem:variablestovariables\], it follows that $\sigma$ is a variable-to-variable substitution, and then from Lemma \[lem:pastingfact\] we conclude that $\Gamma$ is a disc context $\uD^k$ with $k\leq n$, and $\sigma$ is a subdisc inclusion. We therefore conclude that $t \equiv \coh (\uD^k : u \to_T v)[\sigma]$.

Suppose $\dim(t) = k$. Then $u,v$ must each use all the variables of the respective boundary context, so by induction on subterms, the only possibility is $u = d_{k-1}$ and $v = d'_{k-1}$. Since $t$ is not a C-redex, we conclude that $u$ is in normal form (hence $u \equiv d_{k-1}$), $v$ is in normal form (hence $v \equiv d'_{k-1}$), and $T$ is in normal form (hence $T \equiv S^{k-2}$), and so $t \equiv \coh(\uD^k : d_{k-1} \to_{S^{k-2}} d'_{k-1})[\sigma]$. But then $t$ would be a D-redex, which is a contradiction.

So we must have $\dim(t) > k$. Then $u,v$ must each use all the variables of $\uD^k$, so by induction on subterms, the only possibility is $u = v = \i^{n-k}(d_k)$. But this would mean that $t$ is an E-redex, again giving a contradiction.

Rehydration {#sec:rehydration}
===========

#### Overview

The results of Section 3 tell us that normal forms decide definitional equality, in the following sense: $$\begin{aligned}
u = v &\quad\Rightarrow\quad N(u) \equiv N(v)
\intertext{Since normalization contracts definitional equivalence classes, and since $\Catt$ has a trivial notion of definitional equality, we might imagine this is sufficient to produce our encoding function $\rho$ into $\Catt$ terms. However, a normalized valid $\Catt_\su$ term $t$ is \textit{not} necessarily a valid $\Catt$ term. To see why, we note that the property above does not extend to boundaries of terms:}
\tgt(u) = \src(v) &\quad\not \Rightarrow\quad \tgt(N(u)) \equiv \src(N(v))\end{aligned}$$ As a result, if a pair of normalized terms of $\Catt_\su$ are composable, implicit coercion may *still* be required by the type checker to verify that the composite itself type checks.

The solution is to introduce a new notion called *rehydrated normal form*, written $R(N(t))$. Since it is a function of the normal form, it of course also decides definitional equality: $$\begin{aligned}
u = v &\quad\Rightarrow\quad R(N(u)) \equiv R(N(v))
\intertext{However, it also recursively composes the boundaries of all subterms with coherences, which has the effect of putting  those boundaries \textit{themselves} in rehydrated normal form. These coherences can be regarded as ``explicit coercions'', giving a direct structural witness to the change in type. As a result, we gain the following desirable feature:}
\tgt(u) = \src(v) &\quad\Rightarrow\quad \tgt(R(N(u)) \equiv \src(R(N(v))\end{aligned}$$ Since it also acts recursively on the term structure, we are therefore guaranteed that any composable subterms of $R(N(t))$ will be composable on-the-nose. As a result, for any valid $\Catt_\su$ term $t$, the term $R(N(t))$ will be a valid $\Catt$ term, all necessary coercions having been explicitly inserted.

Finally, since the coercions we insert all normalize to the identity, we are guaranteed that $R(N(t)) = t$ in $\Catt_\su$, meaning that the definitional equivalence classes are preserved. If we define $\rho(t) := R(N(t))$, we therefore obtain the encoding function discussed in the introduction, providing a solution to the Identification Paradox for this “toy model” theory.

#### Rehydrated Normal Form

We introduce the following operations on a term $t$ simultaneously by mutual recursion:

-   the *rehydration* $R(t)$, which rehydrates all subterms, and then pads the resulting term;

-   the *padding* $P(t)$, which composes a term at its boundaries to ensure all of its sources and targets are in rehydrated normal form;

-   the *normalizer* $\phi(t)$, a coherence term which provides an explicit equivalence between $t$ and its rehydrated normal form $R(N(t))$.

We first give the definition of rehydration, in terms of the padding operation.

For a valid term $t$ of $\Catt_\su$, its *rehydration* $R(t)$ is defined as follows:

-   $R(x) := x$

-   $R(\coh ( \Gamma : U)[\sigma] \big) := P \big( \coh(\Gamma:R(U))[R(\sigma)] \big)$

On valid types and substitution, rehydration is defined by applying term rehydration to all subterms and subtypes.

We note that $\supp(t) = \supp(R(t))$ for all terms $t$; this follows since padding is the only non-recursive part of the rehydration operation, which composes the term with normalizers, which cannot change the support, as we discuss below underneath Definition \[def:normalizer\].

We next give the definition of padding, in terms of the normalizers of its inferred sources and targets. Since these sources and targets have strictly smaller dimension than the term itself, the mutual recursion between rehydration, padding and normalizers is well-founded. We use the notation $\mathsf{comp_{n,k}}$ for the coherence introduced on page  and encoding the “unbiased” composite of a $n$-dimensional disc $D$ with two $(k+1)$-dimensional discs $S$ and $T$ glued along the $k$-dimensional source and target of $D$, respectively. This coherence is valid in a context with exactly three locally maximal cells corresponding to $D$, $S$ and $T$. It will be convenient for the presentation in this section, therefore, to write this coherence by providing just these three arguments, i.e. $\mathsf{comp_{n,k}}(a,b,c)$, regarding the non-locally maximal arguments as implicit.

\[def:padding\] For a valid $\Catt_\su$ term $\Gamma \vdash t : A$, its *padding* $P(t)$ is obtained by composing at the boundaries to put them into rehydrated normal form. We define $P(t) := P_{\dim A + 1}(t)$, and then:

-   $P_0(t) := t$

-   $P_{k+1}(t) := \mathsf{comp_{\dim(A)+1, k}} \big( \phi(\src_k(t)), P_{k}(t),\phi^{-1}(\tgt_k(t)) \big)$

The constructors $P_k$ each “fix up” the corresponding inferred source and targets of their arguments, so $P_k(t)$ is guaranteed to have $\src_j(P_k(t))$ and $\tgt_j(P_k(t))$ in rehydrated normal form for all $j < k$.

Finally we give the definition of the normalizer, in terms of rehydration.

\[def:normalizer\] For a term $t$ of $\Catt_\su$, valid over some pasting context $\Gamma$ with $\supp(t) = \FV(\Gamma)$, its *normalizer* $\phi(t)$ is the following coherence: $$\begin{aligned}
\phi(t) := \coh \big( \Gamma: R(N(t)) \to_{\ty(u)} t \big) [\id_\Gamma]
\intertext{Its \emph{inverse} $\phi ^{-1}(t)$ is defined with the reversed type, as follows:}
\phi^{-1}(t) := \coh \big( \Gamma: t \to_{\ty(u)} R(N(t))\big) [\id_\Gamma]\end{aligned}$$

By the formation rules for coherences, we note that $\supp(\src(\phi(t))) = \supp(\tgt(\phi(t))) = \FV(\Gamma)$. For this reason, composing a term with a normalizer does not change the support of that term.

#### Properties of Rehydrated Normal Forms

We now verify that terms in rehydrated normal form have the required properties.

\[lem:inferredrehydrated\] The inferred sources and targets of a term in rehydrated normal form are also in rehydrated normal form.

We demonstrate this as follows: $$\begin{aligned}
\src(R(N(t)) &\equiv \src \Big( \comp_{\dim(A)+1, k} \big( \phi(\src_k(t)), P_{k}(t),\phi^{-1}(\tgt_k(t)) \big) \Big)
\\
&\equiv \src(\phi(\src_k(t)))
\\
&\equiv \src(\coh (\Gamma : R(N(\src_k(t))) \to \src_k(t) )[\id_\Gamma])
\\
&\equiv R(N(\src_k(t)))\end{aligned}$$ This completes the proof.

\[cor:infbdrycomp\] If $\tgt^k(R(N(u))) = \src^j(R(N(v)))$ are valid definitionally-equal terms, then they are syntactically equal.

This is immediate, since we showed above that these boundaries are in rehydrated normal form, and if two terms in rehydrated normal form are definitionally equal, they must be syntactically equal.

We now show that a rehydrated normal form $R(N(t))$ a valid  term. A valid $\Catt_\su$ term $t$ will be valid over a number of contexts $\Gamma$; for simplicity, we suppose for the purposes of this theorem that we have chosen such a context with $\supp(t) = \FV(\Gamma)$, that is, for which $\Gamma$ has no extraneous variables. Such a choice can always be made, although we do not prove that formally here.

\[thm:rntcatt\] If $t$ is a valid term of $\Catt_\su$, over some pasting context $\Gamma$ with $\supp(t)=\FV(\Gamma)$, then $R(N(t))$ is a valid term of $\Catt$.

We argue by induction on subterms, and by dimension on terms, which is consistent in this case, since a valid term cannot have a subterm of greater dimension. For variables, the claim is immediate, and we therefore focus on coherence terms $t \equiv \coh(\Gamma :U)[\sigma]$. Supposing such a term is in normal form, its rehydration is as follows: $$R(t) \equiv P(\coh(\Gamma : R(U))[R(\sigma)])$$ The subterms of $R(U)$ and $R(\sigma)$ will be individually in rehydrated normal form, and hence by induction valid in . Since $R$ does not change the support of the term, $R(U)$ will satisfy the free variable condition for $\coh$ term formation, as required.

We next argue that the subterm $t' := \coh(\Gamma:R(U))[R(\sigma)]$ is valid in . Validity of a $\Catt_\su$ term is generated inductively by typing inferences, as described in Section 2. In every case, the hypotheses for these inferences are that certain typing assertions for subterms are valid. From Proposition \[uniquecohtype\] we know that $\Gamma \vdash t:A$ just when $A = \ty(t)$; and so these typing hypotheses can be reduced to hypotheses that certain inferred boundary terms are definitionally equal to others. But for the term $t'$, all subterms are in rehydrated normal form, and we show above in Corollary \[cor:infbdrycomp\] that inferred boundaries of such terms are definitionally equal just when they are syntactically equal. Validity of the term therefore holds in , which differs from $\Catt_\su$ only in having a restricted notion of definitional equality. Since $t'$ is valid in $\Catt$, its inferred sources and targets will also be valid in .

We now argue that $P(t')$ is valid in $\Catt$. We prove this by induction on the parameter $k$ of the padding construction: $$P_{k+1}(t) \equiv \mathsf{comp_{\dim(A)+1, k}} \big( \phi(\src_k(t)), P_{k}(t),\phi^{-1}(\tgt_k(t)) \big)$$ The composition operations $\mathsf{comp_{d,k}}$ are certainly valid terms, as elementary syntactic constructions. By induction, the subterm $P_k(t)$ is valid in . The normalizers in this expression are being computed for terms $\src_k(t)$,$\tgt_k(t)$. While these terms are not themselves in rehydrated normal form, their inferred types $\ty(\src_k(t))$, $\ty(\tgt_k(t))$ *will* be in rehydrated normal form, thanks to the remark following Definition \[def:padding\].

To complete the proof, we must therefore show that if $u$ is some valid term with $\ty(u)$ in rehydrated normal form, then $\phi(u)$ and $\phi^{-1}(u)$ are valid in $\Catt$. We consider the definition of $\phi(u)$: $$\phi(u) := \coh \big( \Gamma: R(N(u)) \to_{\ty(u)} u \big) [\id_\Gamma]$$ Since $\dim(u) < \dim(t)$, we know by induction on dimension that $R(N(u))$ is valid in . We know $u$ arises as an inferred source or target of $t'$, and hence is valid in . We also know $\ty(u)$ is already in rehydrated normal form, and hence $\ty(u) \equiv \ty(R(N(u)))$. So $\phi(u)$ is valid in , as is $\phi^{-1}(u)$.

Finally, we show that the rehydrated normal form is in the same definitional equivalence class of $\Catt_\su$ of the original term.

\[prop:rnt\] If $t$ is a valid term of $\Catt_\su$ over some pasting context, then: $$R(N(t)) = t$$

For a variable, this is immediate, and we therefore focus on coherence terms. We may assume that the result holds on all terms $u$ of strictly smaller dimension than $t$. This allows us to show that such terms have normalizers which are definitionally equal to identities: $$\begin{aligned}
\phi(u) &\equiv \coh (\Gamma : u \to_{\ty(u)} R(N(u)))[\id_\Gamma]
\\
&\xsquig C _{\rt} \coh(\Gamma: N(u) \to_{N(\ty(u))} N(u))[\id_\Gamma]
\\
& \xsquig E \i_{\dim (t)} \ll \{ N(\ty(u)) \}, N(t) \rr\end{aligned}$$ Note that we use the equation $N(R(N(u))) \equiv N(u)$ in the first step, this being a consequence of the conclusion of the theorem applied to $u$, which is of smaller dimension than $t$.

Now, since paddings are constructed from the normalizers of terms of strictly smaller dimension (namely the sources and targets of $t$), we may use the previous result to show that paddings are definitionally equal to the term being padded. This we prove by induction on the parameter $k$ in the definition of the padding composite $P_k$: $$\begin{aligned}
P_{k+1}(t) &\equiv \mathsf{comp_{n, k}}(\phi(\src_k(t)), P_k(t), \phi(\tgt_k(t)))
\\
&\xsquig A _\t \mathsf{comp_{n,k}}(\i_k \ll \tau \rr, t, \i_k \ll \tau \rr)
\\
&\xsquig B_\t \coh(D^n:d_n \to_{S^{n-1}}d_n)[t]
\\
&\xsquig D t
\intertext{Here, $n:=\dim(t)$. As a consequence, we prove by induction on subterms that $N(R(t)) = N(t)$:}
R(t) &\equiv R(\coh ( \Gamma : U)[\sigma] \big)
\\
&\equiv P \big( \coh(\Gamma:R(U))[R(\sigma)] \big)
\\
&=  \coh(\Gamma:R(U))[R(\sigma)]
\\
&= \coh(\Gamma:U)[\sigma]\end{aligned}$$ This completes the proof.

[^1]: University of Cambridge, UK, `ericfinster@gmail.com`

[^2]: Max Planck Institute for Mathematics, Germany, `reutter@mpim-bonn.mpg.de`

[^3]: University of Cambridge, UK, `jamie.vicary@cl.cam.ac.uk`

[^4]: A theory of *weak $\infty$-categories* (also see Section 1.2) is a mathematical formalism for the homotopy theory of composite structures in arbitrary dimensions. A *strictly unital* theory neglects issues related to composing with unit structures; for example, if $f$ is some nontrivial $n$-dimensional structure, and $\i$ is some $n$-dimensional unit structure of the appropriate type, then the composite $f \circ \i$ would evaluate to $f$ on-the-nose.

[^5]: For the type theories we work with in this paper, a *model* is defined to be a functor ${\cat C}^\op \to \Set$ satisfying a certain gluing condition (see Section 2.3), where C is the category that has contexts $\Gamma$ of the theory as objects, and definitional equality classes of substitutions $\sigma : \Gamma \to \Delta$ as morphisms.

[^6]: The theory has been implemented in OCaml, and the implementation provides additional features not described here, such as implicit arguments for notational convenience. It is available online at <https://github.com/ericfinster/catt.io>.

[^7]: It is known that *strict* higher categories, where this coherence data is completely removed, are not sufficiently expressive to model arbitrary phenomena in higher category theory. The challenge is therefore to strictify as far as possible without losing expressivity, but no further; hence the concept of semi-strictness.
