A Type Theory for Strictly
Associative Infinity Categories

Many definitions of weak and strict $\infty$-categories have been proposed. In this paper we present a definition for $\infty$-categories with strict associators, but which is otherwise fully weak. Our approach is based on the existing type theory , whose models are known to correspond to weak $\infty$-categories. We add a definitional equality relation to this theory which identifies terms with the same associativity structure, yielding a new type theory  \(\Cattsa\), for strictly associative $\infty$-categories. We also provide a reduction relation which generates definitional equality, and show it is confluent and terminating, giving an algorithm for deciding equality of terms, and making typechecking decidable.

Our key contribution, on which our reduction is based, is an operation on terms which we call insertion. This has a direct geometrical interpretation, allowing a subterm to be inserted into the head of the term, flatting its syntactic structure. We describe this operation combinatorially in terms of pasting diagrams,  and also show can be characterized as a  pushout of contexts. This allows reasoning about insertion using just its universal property.

§ INTRODUCTION

It has long been known that not every fully weak \(\infty\)-category is equivalent to one which is fully strict<cit.>. While every bicategory (and by extension monoidal category) is equivalent to a strict 2-category (respectively strict monoidal category)citation?, one can show that such an equivalence is not even possible at dimension \(3\), due to an idea involving the Eckmann-Hilton argument<cit.>.

There are three main classes of coherence in a (globular) \(\infty\)-category: Unitors have the form

\[ f \cdot \id \Rightarrow f\]

associators have the form

\[ (f \cdot g) \cdot h \Rightarrow f \cdot (g \cdot h) \]

and interchangers have the form

\[ (a \cdot_n b) \cdot_m (c \cdot_n d) \Rightarrow (a \cdot_m c) \cdot_n (b \cdot_m d)\]

for compositions \(\cdot_n\) and \(\cdot_m\) of different codimensions (i.e. one could be a vertical composition and the other a horizontal composition). The Eckmann-Hilton argument implies that commutativity of scalars can be built from these 3 classes of coherences, and strictness of these coherences gives a strict commutativity of scalars, which in turn implies that not every weak \(\infty\)-category is equivalent to a strict one.

It is therefore clear that any definition of \(\infty\)-category in which all three of these classes is strict is not general enough to model all weak \(\infty\)-categories. However this does not mean that no structure of the category can be strictified, and this leads to the search of a semistrict definition of an \(\infty\)-category, one which is “as strict as possible” while still retaining the full expressivity of fully weak \(\infty\)-categories.

In dimension \(3\), two semistrict definitions have been given:

* Gray categories<cit.> are a definition where everything is strict apart from the interchange laws, which hold only up to isomorphism. It is proven that every tricategory is equivalent to a Gray category.

* <cit.> introduce a definition for monoidal \(2\)-categories (i.e. \(3\)-categories with one object) which have weak units, but all other structure being strict, and show this is equivalent to the fully weak version.

These suggest two approaches to defining semistrict \(\infty\)-categories, one where unitors and associators are strict and interchangers are weak, as in Gray categories, and one where everything but units are strict, which is known as Simpson's conjecture.

Although many definitions of weak \(\infty\)-categories have been given (for example see <cit.>), not many seem to be partially strict. Two of the authors, along with Reutter, have given a definition of a strictly unital \(\infty\)-category<cit.> by putting a reduction relation on the type theory \(\Catt\)<cit.>. Our work, running in parallel to this, uses the same technique but uses a new reduction relation which quotients out by associators instead of unitors.

\(\Catt\) is a type theory for which we can define the models to be \(\infty\)-categories. Recently it has been shown by <cit.>, that the models of this type theory are exactly Grothendieck-Maltsiniotis \(\infty\)-categories<cit.>. In contrast to the more abstract definitions, \(\Catt\) gives us a way to reason about the theory inductively and naturally allows computer assistance for defining and checking terms. By giving a complete reduction (one which is strongly normalising and confluent) we can create a quotient of this theory while retaining its computational properties such as decidable equality of terms and decidable typechecking.

To define our new reduction relation, we introduce an operation which we call “insertion”. This operation effectively combines compound composites into a single composite. The simplest example of this is the standard 1-dimensional associativity equation. If we start with the compound composite \(f \cdot (g \cdot h)\), insertion will combine these into a single ternary composition \(f \cdot g \cdot h\). Similarly the term \((f \cdot g) \cdot h\) will be reduced to the same ternary composition. We call this operation insertion as when we view this as an operation on pasting diagrams, the pasting diagram for the inner composition is inserted into the pasting diagram for the outer composition. We give relatively weak conditions for this insertion to be admissible, and further show that it satisfies a certain universal property.

§.§ Contributions and Future Work

We introduce a type theory \(\Cattsa\) for which the models form strictly associative \(\infty\)-categories. This is done by defining an operation on the structure of the type theory \(\Catt\) called insertion and creating an equality relation based on this. We further prove some properties of this insertion operation, and show that there is a reduction scheme which agrees with the equality and is complete, and hence give algorithms for deciding equality and typechecking.

Further we show that the pruning operation introduced for strict unit normalisation<cit.> can be seen as an instance of our insertion operation, which suggests the two reduction schemes are compatible and can be combined to give a type theory which models strictly associative and unital \(\infty\)-categories. Proving that this reduction scheme is indeed complete is ongoing work.

Finally, we would eventually like to be able to find a connection between our work and associative n-categories<cit.>, which are a far more combinatoric definition of strictly associative and unital higher categories. These have the advantage that they can be viewed and manipulated graphically by contractions<cit.>, and have been implemented in the proof assistant “homotopy.io”<cit.>. We eventually hope to find a strict enough type theoretic definition of higher categories such that associative n-category terms can be converted into the terms of this theory. This would have the two purposes: firstly it gives evidence that the structures manipulated by a tool such as “homotopy.io” really do correspond to conventional definitions of higher categories and secondly could make it easier to construct terms of \(\Catt\) and related theories.

We first define the syntax and typing rules of the base type theory \(\mathsf{Catt}\), which models weak \(\infty\)-categories. Here we give a full account of all the rules of the type theory, and carefully set up how we will add definitional equality into the theory, though do not give much motivation for many of the base roles, for which we encourage the reader to look at the original paper on \(\Catt\)<cit.> or 's PhD thesis<cit.>.

§.§ Syntax

Let \(V\) be an infinite set of variables. Then the syntax of
contexts, substitutions, types, and terms
(written , , , ) is given by:

Γ:  A :  x ∈V
3Γ, (x : A) :

σ:  t :  x : V
3⟨σ, x ↦t ⟩:

A :  s :  t :
3s A t :

x ∈V 1x :

Γ:  A :  σ:
3ΓA σ:

The symbol \(\equiv\) will represent syntactic equality.

We define the support of a term, type, or substitution
in context \(\Delta\) as follows:

* Substitutions: \(\supp_\Delta(\langle \rangle) = \emptyset\),
\(\supp_\Delta(\langle \sigma , t \rangle) = \supp_\Delta(\sigma)
\cup \supp_\Delta(t)\).

* Types: \(\supp_\Delta(\star) = \emptyset\), \(\supp(\arr s A t)
= \supp_\Delta(s) \cup \supp_\Delta(t)\)

* Terms:

_Δ(x)       = {x} ∪_Δ(A)         if \((x:A) \in \Delta\)

_Δ(ΓA σ)       = _Δ(σ)

We Write \(\supp(t)\) when the context is obvious.

A dimension function \(\dim\) on types is defined by:

(⋆)       = 0

(s A t)       = (A) + 1

(∅)       = -1

(Γ, (x : A))       = max((Γ), (A))

And we define partial substitution functions for \(\sigma\, \tau :
\Sub, s\, t : \Term, A : \Type, x \in V\) as well as partial
composition function given by:

⋆σ      = ⋆

(s A t) σ      = s σ A σ t σ         if this is defined

ΓA τ σ      = ΓA τ∘σ       if \(\tau \circ \sigma\) is defined

x σ      = t       if \(x \mapsto t \in \sigma\) and \(x\) only occurs once in \(\sigma\)

⟨⟩∘σ      = ⟨⟩

⟨τ, x ↦t ⟩∘σ      = ⟨τ∘σ, x ↦t σ⟩      if this is
well defined

§.§ Pasting Contexts and Globular Properties

Contexts in \(\mathsf{Catt}\) correspond to finite computads (also known as finite polygraphs). Here we give rules to classify those contexts which form pasting diagrams.

1[$\star$]x : ⋆⊢_pd x : ⋆

Γ⊢_pd x : ⋆ 1[]Γ⊢_pd

Γ⊢_pd x : A y,f ∈V ∖(Γ) 2[$\Uparrow$]Γ, (y : A), (f : x
A y) ⊢_pd f : x A y

Γ⊢_pd f : x A y
1[$\Downarrow$]Γ⊢_pd y : A

Then given a pasting scheme \(\Gamma\), the source
\(\partial^-(\Gamma)\) and target \(\delta^+(\Gamma)\) can be defined:

∂^-(x : ⋆)       = ∅

∂^-(Γ, y : A, f : x A y)       =

∂^-(Γ), y : A, f : x A y   if \(\dim(A) + 1 < \dim(\Gamma)\)

∂^-(Γ)   if \(\dim(A) + 1 = \dim(\Gamma)\)

Γ   if \(\dim(A) + 1 > \dim(\Gamma)\)

(Γ, x : A)       = Γ

∂^+(x : ⋆)       = ∅

∂^+(Γ, y : A, f : x A y)       =

∂^+(Γ), y : A, f : x A y   if \(\dim(A) + 1 < \dim(\Gamma)\)

∂^+((Γ), y : A)   if \(\dim(A) + 1 = \dim(\Gamma)\)

(Γ), y : A   if \(\dim(A) + 1 > \dim(\Gamma)\)

More generally we have the notion of a globular context, which is a context that does not contain any coherences in its syntax tree. These correspond to the computads which are just globular sets.

Given an ambient context \(\Gamma\), we can extend the dimension function to terms.

_Γ(x)       = (A)         if \((x:A) \in \Gamma\)

_Γ(ΔA σ)       = (A)

Further for a term of dimension \(m\), and \(n \leq m\), we can define the \(n^{th}\) source and target of the term as follows.

δ_Γ,n^ϵ(t)       = t         if \(n = \dim(x)\)

δ_Γ,n^ϵ(x)       = A^ϵ_n         if \((x: A) \in \Gamma \) and \(n < \dim(x)\)

δ_Γ,n^ϵ(ΔA σ)       = A^ϵ_n σ        if \(n < \dim(A)\)

As before, the subscript context will be omitted when it can be inferred.

We also introduce a way to deconstruct types:

If \(A\) is a \(n\) dimensional type and \(m < n\) then define \(A^\epsilon_m\) as follows: First note that \(m < n\) so \(n\) is at least \(1\) and so \(A \equiv \arr s {A'} t\).

* If \(m = n - 1\) then \(A^-_m \equiv s\) and \(A^+_m \equiv t\).

* Otherwise \(A^\epsilon_m = {(A')}^\epsilon_m\).

Lastly we define unbiased compositions.

Mutually inductively define the unbiased term and unbiased type of a pasting diagram \(\Gamma\), written \(UTm(\Gamma)\) and \(UTy(\Gamma)\).

* For a disk pasting diagram, the unbiased term is the top-dimensional variable, and the unbiased type is the type of this variable.

* For any other pasting diagram \(\Gamma\), the unbiased type is given by \(UTm(\partial^-(\Gamma)) \to UTm(\partial^+(\Gamma))\) and the unbiased term is given by \(\Coh \Gamma {UTy(\Gamma)} \id\)

A coherence \(\Coh \Delta A \sigma\) is unbiased if \(A\) is the unbiased type over \(\Delta\).

§.§ Properties of Syntax

We will now introduce some auxiliary definitions on the syntax of \(\mathsf{Catt}\). To do we want to consider an arbitrary type theory based on the syntax. This must contain a notion of definitional equality, and typing judgments.

A congruence \(\sim\) is a tuple of equivalence relations on contexts, terms, substitutions and types. By abuse of notation we call all 4 of these relations \(\sim\). We then must have the following rules:

Γ∼Γ' A ∼A'
2Γ, (x : A) ∼Γ', (x : A')

σ∼σ' t ∼t'
2⟨σ, x ↦t ⟩∼⟨σ', x ↦t' ⟩

A ∼A' s ∼s' t ∼t'
3s A t ∼s' A' t'

Γ∼Γ' A ∼A' σ∼σ'
3ΓA σ∼Γ' A' σ'

Syntactic equality, \(\equiv\), is a congruence.

We can now define the notion of a \(\mathsf{Catt}\)-based type theory.

A \(\mathsf{Catt}\)-based type theory consists of a congruence \(=\), and typing judgments:

* \(\Gamma \vdash\)

* \(\Gamma \vdash A\)

* \(\Gamma \vdash \sigma : \Delta\)

* \(\Gamma \vdash t : A\)

for contexts \(\Gamma\) and \(\Delta\), type \(A\), substitution \(\sigma\), and term \(t\). We further require that the following rules are satisfied:

Γ⊢ Γ= Γ'
2Γ' ⊢

Γ⊢A Γ= Γ' A = A'
3Γ' ⊢A

Γ⊢σ: Δ Γ= Γ' σ= σ' Δ= Δ'
4Γ' ⊢σ' : Δ'

Γ⊢t : A Γ= Γ' t = t' A = A'
4Γ' ⊢t' : A'

§.§ Typing for \(\mathsf{Catt}\)

To define the base type theory \(\mathsf{Catt}\), we need to define the definitional equality, and the typing judgments. The definitional equality will just be given by reflexivity. The typing rules for contexts, substitutions and types are given by:

Γ⊢ x ∈V ∖(Γ)
Γ⊢A 3Γ, (x : A) ⊢

Γ⊢ 1Γ⊢⋆

Γ⊢A Γ⊢s : A Γ⊢t : A 3Γ⊢s A t

1Δ⊢⟨⟩: ∅

Δ⊢σ: Γ Γ⊢A
Δ⊢t : A σ x ∈V ∖(Γ) 4Δ⊢⟨σ, x ↦t ⟩: Γ, (x : A)

and then the rules for terms are given by:

Γ⊢ (x : A) ∈Γ
2[\((\text{var})\)]Γ⊢x : A

Γ⊢s A t
Δ⊢σ: Γ
(s) = ∂^-(Γ)
(t) = ∂^+(Γ)
5[\((\text{comp})\)]Δ⊢Γ(s A t) σ: (s A t) σ

Γ⊢_pd Γ⊢A Δ⊢σ: Γ (A) = Γ
4[\((\text{coh})\)]Δ⊢ΓA σ: A σ

With a definitional equality given by syntactic equality, \(\mathsf{Catt}\) forms a \(\mathsf{Catt}\)-based type theory.

§ INSERTION

Now that we have defined the base type theory \(\Catt\), we are in a position to describe our insertion operation. We will first give an intuition to the action of this operation. Suppose we have the term \(a \cdot (b \cdot c)\), where \(a \cdot b\) represents (leaving out some implicit terms in the substitution):

\[ \Coh {(x : \star) (y : \star) (f : x \to y) (z : \star) (g : y \to z)} {x \to z} {f \mapsto a, g \mapsto b}\]

In this case we are composing over some pasting diagram, and then one of the (locally maximal) arguments to this pasting diagram is itself a composition over a pasting diagram, in this case the variable \(g\). Insertion then removes the variable \(g\) and everything in its support and “inserts” the inner pasting diagram in its place. This is demonstrated in <ref> (where we have alpha renamed the inner pasting diagram to reduce confusion), where the final pasting diagram is simply giving the ternary composite, the unbiased version of the original composite.

To fully describe the new term, we also need two more constructions, as the coherence term constructor has three parts. Firstly we need a new substitution from the new pasting context to the ambient context, which assigns the arguments to the new composition. This can simply be done by mapping parts of the original pasting diagram (those in black in the figure) to their original arguments, and the parts of the inner pasting diagram (those in red in the figure) to the arguments of the inner composition. Secondly we need to construct the type part of the coherence (the \(A\) in \(\Coh \Gamma A \sigma\)). The most obvious way to do this is to transport the old type to the new pasting diagram, which will require a substitution from the old pasting diagram to the new inserted one.

\[\begin{tikzcd}
x & y & z && \textcolor{rgb,255:red,255;green,0;blue,0}{x'} & \textcolor{rgb,255:red,255;green,0;blue,0}{y'} & \textcolor{rgb,255:red,255;green,0;blue,0}{z'}
\arrow["f", from=1-1, to=1-2]
\arrow[""{name=0, anchor=center, inner sep=0}, "g", from=1-2, to=1-3]
\arrow["{f'}", color={rgb,255:red,255;green,0;blue,0}, from=1-5, to=1-6]
\arrow["{g'}", color={rgb,255:red,255;green,0;blue,0}, from=1-6, to=1-7]
\arrow[curve={height=30pt}, shorten <=12pt, shorten >=12pt, Rightarrow, 2tail reversed, no head, from=0, to=1-6]
\end{tikzcd}\]

is sent to:

\[\begin{tikzcd}
x & \textcolor{rgb,255:red,255;green,0;blue,00}{x'} & \textcolor{rgb,255:red,255;green,0;blue,0}{y'} & \textcolor{rgb,255:red,255;green,0;blue,0}{z'}
\arrow["{f'}", color={rgb,255:red,255;green,0;blue,0}, from=1-2, to=1-3]
\arrow["{g'}", color={rgb,255:red,255;green,0;blue,0}, from=1-3, to=1-4]
\arrow["f", from=1-1, to=1-2]
\end{tikzcd}\]

Insertion on \(a \cdot (b \cdot c)\)

Our insertion operation needs to trivialise associativity at all dimensions and all codimensions, and needs to consider composites of any shape so that the operation is natural enough to be confluent. Although the example we gave is relatively simple, describing the general operation at all dimensions can be tricky to reason about and so we will represent our pasting diagrams as labelled Batanin trees.

Given a set of variables \(\L\), a \(\L\)-labelled Batanin trees, \(T\) can be defined inductively as a tuple \((T_l,T_b)\) where \(T_l\) is a list of labels contained in \(\L\), \(T_b\) is a list of \(\L\) labelled Batanin trees, and further the length of \(T_l\) is one greater than the length of \(T_b\).

From every labelled Batanin tree, we can obtain a context, and further show that this context is a pasting diagram. Given a tree \(T\), we will denote the context \(\lfloor T \rfloor\).

Given a context \(\Gamma\), with a proof that it is a pasting diagram, we can form a labelled Batanin tree \(\lceil \Gamma \rceil\). Further we have \(\lfloor \lceil \Gamma \rceil \rfloor = \Gamma\) and \(\lceil \lfloor T \rfloor \rceil = T\) for all pasting diagrams \(\Gamma\) and trees \(T\).

See <cit.>

The linear height of a Batanin tree is the height of the tree before any branches occur. It can be defined recursively as:

\begin{equation*}
\mathsf{lh}((T_l,T_b)) =
\begin{cases}
1 + \mathsf{lh}(t) &\text{if } T_b = [ t ],\\
0 &\text{otherwise}
\end{cases}
\end{equation*}

A tree is generated from a pasting context by having the labels be the \(0\)-dimensional cells of the pasting diagram and then the tree between each 2 labels be the part of the pasting diagram suspended between those two labels. Consider these two examples, which we call \(\Delta\) and \(\Theta\):

Pasting diagram     Batanin tree
\(\Delta\)    20pt[ampersand replacement = &]
x && y & z
[from=1-3, to=1-4, "k"]
[""name=0, anchor=center, inner sep=0, "g"pos=0.7, from=1-1, to=1-3]
[""name=1, anchor=center, inner sep=0, "f"', curve=height=18pt, from=1-1, to=1-3]
[""name=2, anchor=center, inner sep=0, "h", curve=height=-18pt, from=1-1, to=1-3]
["β", shorten <=2pt, shorten >=2pt, Rightarrow, from=0, to=2]
["α", shorten <=2pt, shorten >=2pt, Rightarrow, from=1, to=0]

[every node/.style=scale=0.8]
[label=left:$x$,label=right:$z$,on grid](x01) $\bullet$;
[label=left:$f$,label=right:$h$,above left=0.7 and 0.4 of x01, on grid] (x11) $\bullet$;
[label=above:$k$,above right=0.7 and 0.4 of x01, on grid] (x12) $\bullet$;
[label=above:$\alpha$,above left=0.7 and 0.25 of x11, on grid] (x21) $\bullet$;
[label=above:$\beta$,above right=0.7 and 0.25 of x11, on grid] (x22) $\bullet$;
at ($0.65*(x01) + 0.175*(x11) + 0.175*(x12)$) $y$;
at ($0.65*(x11) + 0.175*(x21) + 0.175*(x22)$) $g$;
(x01.center) to (x11.center);
(x01.center) to (x12.center);
(x11.center) to (x21.center);
(x11.center) to (x22.center);

\(\Theta\)   20pt [ampersand replacement=&]
x' && y'
[""name=0, anchor=center, inner sep=0, "g'"pos=0.7, from=1-1, to=1-3]
[""name=1, anchor=center, inner sep=0, "f'"', curve=height=18pt, from=1-1, to=1-3]
[""name=2, anchor=center, inner sep=0, "h'", curve=height=-18pt, from=1-1, to=1-3]
["β'", shorten <=2pt, shorten >=2pt, Rightarrow, from=0, to=2]
["α'", shorten <=2pt, shorten >=2pt, Rightarrow, from=1, to=0]

[every node/.style=scale=0.8]
[label=left:$x'$,label=right:$y'$,on grid](x01) $\bullet$;
[label=left:$f'$,label=right:$h'$,above=0.7 of x01, on grid] (x11) $\bullet$;
[label=above:$\alpha'$,above left=0.7 and 0.25 of x11, on grid] (x21) $\bullet$;
[label=above:$\beta'$,above right=0.7 and 0.25 of x11, on grid] (x22) $\bullet$;
at ($0.65*(x11) + 0.175*(x21) + 0.175*(x22)$) $g'$;
(x01.center) to (x11.center);
(x11.center) to (x21.center);
(x11.center) to (x22.center);

Here the first has a linear height of \(0\) and the second has a linear height of \(1\).

Each label in a Batanin tree can be associated with a path (a non empty list of natural numbers) specifying how to reach that label from the root of the tree. A path in a Batanin tree is valid if it is the path associated with one of the tree's labels.

Given a tree \(T\) and a locally maximal variable \(x\), we can define the branching path of this variable, which we think of as the path to the last branching in the tree before reaching this variable, as follows: If \(T_b\) is empty then we return the path \([0]\). Otherwise \(T_b\) is not empty and as \(x\) is locally maximal, it must occur in the \(n\)th branch of \(T_b\) for some \(n\). If this branch is linear then we return \([n]\), otherwise we append \(n\) to the branching path of \(x\) in this branch.

Write \(A^{[i..j]}\) for the list consisting of the \(i\)th element of \(A\) to the \(j\)th element of \(A\) (zero indexing).
Suppose \(S\) and \(T\) are Batanin trees, and \(p\) is a valid path in \(S\), and \(\mathsf{lh}(T) \geq \mathsf{length}(p) - 1\). Then we define the insertion of \(T\) into \(S\) along path \(p\), written \(\insertion S p T\), by recursion on \(p\).

Suppose \(p = [n]\), then let \({(\insertion S p T)}_l\) be equal to \(S_l^{[0..(n-1)]} \doubleplus T_l \doubleplus S_l^{[(n+2)..]}\) and \({(\insertion S p T)}_b\) be equal to \(S_b^{[0..(n-1)]} \doubleplus T_b \doubleplus S_b^{[(n+1)..]}\).

Suppose instead \(p\) has head \(n\) and non empty tail \(p'\). By the linearity condition we have that \(T_b = [T']\) for some \(t\) and let the \(n\)th element of \(S_b\) be \(S'\). Then again let \({(\insertion S p T)}_l = S_l^{[0..(n-1)]} \doubleplus T_l \doubleplus S_l^{[n+2..]}\) and in this case let \({(\insertion S p T)}_b = S_b^{[0..(n-1)]} \doubleplus [ \insertion S' p' T' ] \doubleplus S_b^{[(n+1)..]}\).

Finally for contexts \(\Delta\) and \(\Theta\), and some locally maximal variable \(x\) of \(\Delta\), let \(\insertion \Delta x \Theta = \lfloor \insertion {\lceil \Delta \rceil} p {\lceil \Theta \rceil} \rfloor\) where \(p\) is the branching path of \(x\).

The internal substitution from \(\iota_{\Delta,x,\Theta} : \Theta \to \insertion \Delta x \Theta\) is given my mapping each variable to itself.

The linear height of a type \(A\) is the maximum \(n\) such that all terms contained in \(A\) with dimension less than or equal to \(A\) are variables.

Given a type \(A\) with \(\Delta \vdash A\) with linear height at least one less than the length of the branching path length of \(x\), we can define the external substitution \(\kappa_{\Delta,x,\Theta,A} : \Delta \to \insertion \Delta x \Theta\) by sending a variable \(y\) to \(y\) if variable \(y\) is in \(\insertion \Delta x \Theta\) and otherwise \(y\) is \(\delta^\epsilon_n(x)\) for some \(\epsilon \in \{+,-\}\) and \(n\), and then we can map \(y\) to \(\delta^\epsilon_n(\Coh {\Theta} A {\iota_{\Delta,x,\Theta}})\).

Suppose we have contexts \(\Delta\) and \(\Theta\) from <ref>. The variable \(\alpha\) has a branching height of \(1\) in \(\Delta\), and \(\Theta\) has a linear height of \(1\), so the insertion \(\insertion \Delta \alpha \Theta\) is well defined and is given in <ref> as a pasting diagram and as a tree. The internal substitution \(\iota_{\Delta,\alpha,\Theta}\) maps \(\Theta\) into the part of \(\insertion \Delta \alpha \Theta\) marked in red by mapping each variable to itself.

If we take \(A\) to be \(f \cdot k \to h \cdot k\), then \(\Delta \vdash A\) and \(A\) has linear height \(1\) and so we can define the external substitution \(\kappa_{\Delta,\alpha,\Theta,A}\) which has the following action:

0-cells:     \(x \mapsto x'\quad y \mapsto y'\quad z \mapsto z\)

1-cells:     \(f \mapsto f'\quad g \mapsto h'\quad h \mapsto h\quad k \mapsto k\)

2-cells:     \(\alpha \mapsto \Coh \Theta A \iota\quad \beta \mapsto \beta\)

[ampersand replacement=&]
x' && y' & z
[from=1-3, to=1-4,"k"]
[""name=0, anchor=center, inner sep=0, "h'"pos=0.6, color=rgb,255:red,255;green,0;blue,0, curve=height=-12pt, from=1-1, to=1-3]
[""name=1, anchor=center, inner sep=0, "f'"', color=rgb,255:red,255;green,0;blue,0, curve=height=30pt, from=1-1, to=1-3]
[""name=2, anchor=center, inner sep=0, "h", curve=height=-30pt, from=1-1, to=1-3]
[""name=3, anchor=center, inner sep=0, "g'"pos=0.8, color=rgb,255:red,255;green,0;blue,0, curve=height=12pt, from=1-1, to=1-3]
["β", shorten <=2pt, shorten >=2pt, Rightarrow, from=0, to=2]
["α'", color=rgb,255:red,255;green,0;blue,0, shorten <=2pt, shorten >=2pt, Rightarrow, from=1, to=3]
["β'", color=rgb,255:red,255;green,0;blue,0, shorten <=3pt, shorten >=3pt, Rightarrow, from=3, to=0]

[every node/.style=scale=0.8]
[color=red,label=[red]left:$x'$,label=right:$z$,on grid](x01) $\bullet$;
[color=red,label=[red]left:$f'$,label=right:$h$,above left=0.7 and 0.4 of x01, on grid] (x11) $\bullet$;
[label=above:$k$,above right=0.7 and 0.4 of x01, on grid] (x12) $\bullet$;
[color=red,label=[red]above:$\alpha'$,above left=0.7 and 0.5 of x11, on grid] (x21) $\bullet$;
[label=above:$\beta$,above right=0.7 and 0.5 of x11, on grid] (x23) $\bullet$;
[color=red,label=[red]above:$\beta'$,above=0.7 of x11, on grid](x22) $\bullet$;
[red] at ($0.65*(x01) + 0.175*(x11) + 0.175*(x12)$) $y'$;
[red] at ($0.5*(x11) + 0.2*(x21) + 0.3*(x22)$) $g'$;
[red] at ($0.5*(x11) + 0.3*(x22) + 0.2*(x23)$) $h'$;
[red] (x01.center) to (x11.center);
(x01.center) to (x12.center);
[red] (x11.center) to (x21.center);
[red] (x11.center) to (x22.center);
(x11.center) to (x23.center);

The insertion of \(\Theta\) into \(\Delta\)

Given \(\sigma : \Delta \to \Gamma\), \(\tau : \Theta \to \Gamma\), and variable \(x\) in \(S\), we define the inserted substitution \(\insertion \sigma x \tau : \insertion \Delta {x} \Theta \to \Gamma\), as sending any variable \(y\) originating from \(S\) to \(\sigma(y)\) and any variable \(y\) originating from \(T\) to \(\tau(y)\).

Subscripts from the external and internal substitutions may be dropped when there is no ambiguity.

§.§ \(\Cattsa\)

We define the type theory \(\Cattsa\) as having the same syntax as \(\Catt\). In addition to \(\Catt\) it will have an extra definitional equality and modify the typing rules for terms. These will be defined simultaneously, though this will be well founded as the typing for a term will only depend on equality for terms of lower dimension and equality of terms will only depend on typing of terms of the same dimension.

The definitional equality will be given by the smallest congruence such that for all well typed terms \(\Coh \Delta A \sigma\), locally maximal variable \(x\) of \(\Delta\) with \(\sigma(x)\) equal to an unbiased composite \(\Coh \Theta B \tau\) with the branching height of \(x\) is less than or equal to the linear height of \(\Theta\) we have:

\[\Coh \Delta A \sigma = \Coh {\insertion \Delta x \Theta} {\sub A {\kappa_{\Delta,x,\Theta}}} {\insertion \sigma x \tau} \]

Explicitly, the definitional equality will have the following structural rules:

1∅= ∅

Γ= Γ' A = A'
2Γ, x : A = Γ', x : A'

1⋆= ⋆

A = A' s = s' t = t'
3s A t = s' A' t'

1⟨⟩= ⟨⟩

σ= σ' t = t'
2⟨σ, x ↦t ⟩= ⟨σ', x ↦t' ⟩

t = t'
1t' = t

t = t' t' = t”
2t = t”

1x = x

A = A' σ= σ'
2ΔA σ= ΔA' σ'

This definitional equality is a congruence.

We then modify the typing rules for terms to the following:

Γ⊢ (x : A) ∈Γ A = B
3[\((\text{var}')\)]Γ⊢x : B

Γ⊢_pd   Γ⊢s A t   Δ⊢σ: Γ

(s) = ∂^-(Γ)   (t) = ∂^+(Γ)   B = (s A t) σ

1[\((\text{comp}')\)]Δ⊢Γ(s A t) σ: B

Δ⊢σ: Γ
(A) = Γ
B = A σ
5[\((\text{coh}')\)]Δ⊢ΓA σ: B

From these rules we can deduce that the following conversion rule is admissable:

Γ⊢t : A A = B
2Γ⊢t : A'

Next, we will prove that the constructions make some form of sense, in that the constructed substitutions are indeed well typed in \(\Cattsa\). We start with the following definition.

A substitution \(\sigma\) from a globular set \(\Gamma\) to arbitrary context \(\Delta\) respects the globular conditions if for all \(x : \arr s A t\) in \(\Gamma\), we have \(\delta^-(\sigma(x)) = \sigma(s)\) and \(\delta^+(\sigma(x)) = \sigma(t)\). Say a substitution is well-formed if it respects the globular conditions and maps each variable of \(\Gamma\) to a term which is well typed in \(\Delta\).

If \(\Delta \vdash u : A\) then \(\delta^\epsilon_n(u) = A^\epsilon_n\) for all \(n < \dim(A)\).

Proceed by induction on the proof of \(\Delta \vdash u : A\).

* If it is proved using a variable rule, then the result follows straight from definition of \(\delta\) and compatibility of \({(-)}^\epsilon_n\) and equality.

* If it is proved with the coherence or comp rule then \(u \equiv \Coh \Gamma B \sigma\) and \(A = \sub B \sigma\). Then \(\delta^\epsilon_n(u) \equiv \sub {B^\epsilon_n} \sigma \equiv {(\sub B \sigma)}^\epsilon_n = A^\epsilon_n\).

In \(\Cattsa\), if \(\Gamma\) is a globular set then \(\Delta \vdash \sigma : \Gamma\) if and only if \(\sigma\) is well-formed.

Proceed by induction on the length of \(\sigma\). If \(\sigma\) is empty, then it is both well-formed and well-typed.

Now consider \(\langle \sigma, x \mapsto u \rangle\) and first suppose \(\Delta \vdash \langle \sigma, x \mapsto u \rangle : \Gamma, x : A\). By inductive hypothesis, \(\sigma\) is well-formed. In particular each variable of \(\Gamma\) is sent by \(\sigma\) to a well-typed term of \(\Delta\). Further, by assumption \(\Delta \vdash u : \sub A \sigma\) and so \(x\) is also sent to a well-typed term. Now we need to show this substitution respects the globular conditions. The only case that does not immediately follow from inductive hypothesis is the one for \(x\). If \(A \equiv \star\) then there is nothing to do. Otherwise suppose \(A \equiv \arr s {A'} t\). Then \(\Delta \vdash u : \arr {\sub s \sigma} {\sub {A'} \sigma} {\sub t \sigma}\). Then by <ref> we have \(\delta^-(u) = \sub s \sigma\) and \(\delta^+(u) = \sub t \sigma\) as required.

Now suppose \(\langle \sigma, x \mapsto u \rangle\) is well-formed. As a well-formed substitution maps all the variables in the source context, we must have \(x : A \in \Gamma\). Then we have that \(\Delta \vdash u : B\) for some type \(B\) by the substitution being well-formed. If \(B \equiv \star\) then \(A\) must also be \(\star\) so we are done. Otherwise, for all \(\epsilon\) and \(n\), we have that \(\delta^\epsilon_n(u) = B^\epsilon_n\) by <ref> and \(\delta^\epsilon_n(u) = \sub {A^\epsilon_n} \sigma\) by \(\sigma\) being well formed. Therefore \(\sub A \sigma = B\) and so \(\Delta \vdash u : \sub A \sigma\) by an application of the conversion rule.

We now introduce a further equality operation, which effectively says that two terms are definitionally equal but also syntactically equal on any part of the term which has suitably high dimension. This will be useful later for proving confluence.

Define the equality relation \(=_n\) on terms, types, and substitutions by the following rules.

* If \(s\) and \(t\) are terms with \(\dim(s) < n\) and \(\dim(t) < n\) then \(s =_n t\) if and only if \(s = t\).

* If \(s\) is a variable of dimension greater than or equal to \(n\) then \(s =_n t\) if and only if \(s \equiv t\).

* If \(s \equiv \Coh \Delta A \sigma\) with \(\dim(s) \geq n\) then \(s =_n t\) if and only if \(t \equiv \Coh {\Delta} {A'} {\sigma'}\) and \(A =_n A'\) and \(\sigma =_n \sigma'\).

* For types \(\star =_n \star\) and \(\arr s A t =_n \arr {s'} {A'} {t'}\) if and only if \(s =_n s'\), \(t =_n t'\), and \(A =_n A'\).

* For substitutions \(\langle t_0, \dots, t_k \rangle =_n \langle s_0, \dots, s_k \rangle\) if and only if \(t_i =_n s_i\) for all \(i\).

Next fix pasting contexts \(\Delta\) and \(\Theta\), a variable \(x\) in \(\Delta\), and a type \(A\) with \(\Theta \vdash A\), such that the linear height of \(A\) is at least one less than the branching height of \(x\).

\(\iota : \Theta \to \insertion \Delta x \Theta\) is well-formed.

As all the variables in \(\Theta\) have the same type in the inserted context, this is clearly a well-formed substitution.

The substitution \(\kappa : \Delta \to \insertion \Delta x \Theta\) is well-formed.

For this to be a well-formed substitution, the only interesting case is where \(y\) is not in the support of \(x\), yet one or both of it's source and target variables are. Suppose variable \(z\) is the target of \(y\) and the \(n\)th source of \(x\) in \(\Delta\). An inspection of the algorithm shows that the target of \(y\) in \(\insertion \Delta x \Theta\) is the unique variable in the \(n\)th source of \(\Theta\), which we call \(z'\). However now we have that \(\kappa(z) \equiv \delta^-_n(\Coh \Theta A \iota) \equiv z' \equiv \delta^-(y)\) and so \(\kappa(\delta_\Delta^-(y)) \equiv \delta_{\insertion \Delta x \Theta}^-(\kappa(y))\). The case where \(z\) was the source of \(y\) follows similarly.

Now further assume that we have well-formed \(\sigma : \Delta \to \Gamma\) and \(\tau : \Theta \to \Gamma\) with \(\sigma(x) = \Coh \Theta A \tau\).

\(\tau = (\insertion \sigma x \tau) \circ \iota\) and \(\sigma = (\insertion \sigma x \tau) \circ \kappa\).

The first equality follows directly from the definition of \(\insertion \sigma x \tau\). To prove the second, it suffices to prove the cases for \(y\) in the support of \(x\), as the rest hold definitionally. If \(y = \delta^{\epsilon}_n(x)\), then \(\kappa(y) = \delta^{\epsilon}_n(\Coh \Theta A {\iota})\). Further we know that, as \(\sigma(x) = \Coh \Theta A \tau\) and as all the substitutions are well-formed, \(\sub y \sigma\) is equal to \(\delta^\epsilon_n(\Coh \Theta A \tau)\). Therefore:

\begin{align*}
\sub y \sigma &= \delta_n^\epsilon(\Coh \Theta A \tau)\\
&= \sub {\delta_n^\epsilon(\Coh \Theta A \id)} {\tau}\\
&= \sub {\delta_n^\epsilon(\Coh \Theta A \id)} {(\insertion \sigma x \tau) \circ \iota}\\
&= \sub {(\sub {\delta_n^\epsilon(\Coh \Theta A \id)} {\iota})} {\insertion \sigma x \tau}\\
&= \sub {(\delta_n^\epsilon(\Coh \Theta A {\iota}))} {\insertion \sigma x \tau}\\
&= \sub {(\sub y {\kappa})} {\insertion \sigma x \tau} \\
&= \sub y {(\insertion \sigma x \tau) \circ \kappa}
\end{align*}

and so we get the required syntactic equality.

\(\insertion \sigma x \tau\) is well-formed.

To check that \(\insertion \sigma x \tau\) is well-formed, we again look at the one problematic case where \(y\) originates from \(\Delta\) yet its (without loss of generality) target \(z\) originates from \(\Theta\). Then we need to show that \(\delta^+(\sigma(y)) = \tau(z)\). But then as \(\kappa\) is a well-formed substitution we have that there is \(z' = \delta_\Delta^+(y)\) with \(\kappa(z') = z\). As \(\sigma\) is well-formed we have that \(\delta^+(\sigma(y)) = \sigma(z') = \sub {(\kappa(z'))} {\insertion \sigma x \tau} = (\insertion \sigma x \tau)(z) = \tau(z)\) as required.

§.§ Universal Property of Insertion

We first must introduce some theory about disk contexts:

Recursively define the disk contexts \(D_n\) as \(D_0\) being the context \(d_0^- : \star\) and \(D_{n+1}\) being the context \(D_n, d_n^+ : d_{n-1}^- \to d_{n-1}^+, d_{n+1}^- : d_n^- \to d_n^+\).

Note that each disk context has a single maximal dimension cell, and any substitution out of a disk context is fully determined by where this cell is sent.

A substitution \(D_n \to \Gamma\) is fully determined by its action on \(d_n^-\). If \(\Gamma \vdash t\) and \(t\) is \(n\)-dimensional, then let \(\overline t : D_n \to \Gamma\) be the substitution that sends \(d_m^\epsilon\) to \(\delta_m^\epsilon(t)\) (and so in particular sends \(d_n^-\) to \(t\)).

Given pasting contexts \(\Delta\) and \(\Theta\), a variable \(x\) in \(\Delta\) and a type \(A\) with \(\Theta \vdash A\), we can classify insertion by a universal property.

When \(\dim(A) = \dim(x) = n\), we say that an insertion of \((\Theta,A)\) into \(\Delta\) via \(x\) is the following pushout:

\[\begin{tikzcd}
{D_n} & \Delta \\
\Theta & I
\arrow["{\overline {\Coh \Theta A \id}}"', from=1-1, to=2-1]
\arrow["\overline x"', from=1-1, to=1-2]
\arrow[from=2-1, to=2-2]
\arrow[from=1-2, to=2-2]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=180}, draw=none, from=2-2, to=1-1]
\end{tikzcd}\]

Note that as a pushout, this notion is unique up to isomorphism. If we further require that the insertion is a pasting diagram, then (if it exists) this uniquely specifies this colimit.

When \(\dim(A) = \dim(x) = n\), \(x\) is locally maximal, and \(A\) is linear up to at least one less than the length of the branching path of \(x\), then the following is a pushout in \(\Cattsa\):

\[\begin{tikzcd}
{D_n} & \Delta \\
\Theta & {\insertion \Delta x \Theta}
\arrow["{\overline {\Coh \Theta A \id}}"', from=1-1, to=2-1]
\arrow["\overline x"', from=1-1, to=1-2]
\arrow["{\iota}", from=2-1, to=2-2]
\arrow["{\kappa}"', from=1-2, to=2-2]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=180}, draw=none, from=2-2, to=1-1]
\end{tikzcd}\]

and hence \(\insertion \Delta x \Theta\) is an insertion of \((\Theta,A)\) into \(\Delta\) along \(x\). Further it is a pasting diagram and so is the unique pasting diagram with this property.

We have already checked that all these contexts and substitutions are well typed. To check commutativity of the square it suffices to check that the maximal variable is sent to the same term by each substitution. Along the top it is sent to \(\sub x {\kappa}\), which is defined to be \(\Coh{\Theta} A {\iota} = \sub {(\Coh \Theta A \id)} {\iota}\), which is the term it is sent to along the bottom.

Now suppose that we have \(\Gamma\), \(\sigma\), and \(\tau\) such that the following commutes:

\[
\begin{tikzcd}
{D_n} & \Delta \\
\Theta & {\insertion \Delta x \Theta} \\
&& \Gamma
\arrow["{\Coh \Theta A \id}"', from=1-1, to=2-1]
\arrow["x"', from=1-1, to=1-2]
\arrow["{\iota}", from=2-1, to=2-2]
\arrow["{\kappa}"', from=1-2, to=2-2]
\arrow["\sigma", curve={height=-18pt}, from=1-2, to=3-3]
\arrow["\tau"', curve={height=18pt}, from=2-1, to=3-3]
\end{tikzcd}
\]

Then we need to generate a substitution \(\insertion \Delta x \Theta \to \Gamma\), for which we can give \(\insertion \sigma x \tau\). Any variable \(l\) that originates from \(\Delta\) must be sent to \(\sigma(l)\) and any variable \(l\) that originates from \(\Theta\) must be sent to \(\tau(l)\). This ensures uniqueness. The commutativity conditions are given in <ref>.

To finish this section we note that the conditions we have required for insertion to work are much weaker than what we have used for the definition of \(\Cattsa\). Firstly, for the equality in \(\Cattsa\), we require that the inner term be fully unbiased instead of its type being linear up to a certain height, and further the insertion operation does not depend on the inner term being a composition instead of a coherence, which we explore in the next example.

Suppose we have pasting diagram \(\Delta\) with locally maximal \(x\), and \(\sigma : \Delta \to \Gamma\) with \(\sigma(x) \equiv \id(t)\). Then the pasting diagram of \(\id(t)\) is \(D_n\) for some \(n\). As \(D_n\) is fully linear, it satisfies the conditions for insertion, and so we can form the insertion \(\insertion \Delta x {D_n}\) and from a term \(\Coh \Delta A \sigma\), we could form the term \(\Coh {\insertion \Delta x {D_n}} {\sub A \kappa} {\insertion \sigma x {\overline t}}\). This term has the same form[The two operations are not identical, as inserting an identity takes as many arguments from the inner term as possible, and pruning discards these arguments, taking them from the outer term instead. However, the normal forms of these two operations (with appropriate structural rules) should be identical.] as the result of applying the pruning operation from <cit.> to the original term.

That pruning can be realised as a case of insertion has two exciting consequences. Firstly, this means that we can also realise pruning as a universal property, which was not previously known and allows some proofs to be written in a neat way. It also suggests that the two operations should be compatible and it is possible that they can be combined to get a strictly associative and unital type theory. Proving confluence of such a system is ongoing work.

§.§ Properties of equality

We can now prove some facts about the equality of \(\Cattsa\).

Suppose there exists an insertion of \((\Theta,A)\) into \(\Delta\) and we have substitutions \(\rho : \Delta \to \Gamma\), \(\tau : \Theta \to \Gamma\) and \(\sigma : \Gamma \to \Gamma'\) with \(\rho(x) = \Coh \Theta A \tau\). Then \(\sigma \circ (\insertion \rho x \tau) = \insertion {(\sigma \circ \rho)} x {(\sigma \circ \tau)}\).

Take \(y \in \Var(\insertion \Delta x \Theta)\). If \(y \in \Var(\Theta)\) then:

\begin{align*}
(\sigma \circ (\insertion \rho x \tau))(y) &= \sub {((\insertion \rho x \tau)(y))} {\sigma}\\
&= \sub {(\tau(y))} {\sigma}\\
&= (\sigma \circ \tau)(y)\\
&= (\insertion {(\sigma \circ \rho)} x {\sigma \circ \tau})(y)
\end{align*}

If \(y \in \Var(\Delta)\) then:

\begin{align*}
(\sigma \circ (\insertion \rho x \tau))(y) &= \sub {((\insertion \rho x \tau)(y))} {\sigma}\\
&= \sub {(\rho(y))} {\sigma}\\
&= (\sigma \circ \rho)(y)\\
&= (\insertion {(\sigma \circ \rho)} x {\sigma \circ \tau})(y)
\end{align*}

As these are the only two cases, this completes the proof.

For all well typed \(\sigma = \sigma'\) we have:

* \(\sub t \sigma = \sub {t'} {\sigma'}\) for all well typed terms \(t = t'\)

* \(\sub A \sigma = \sub {A'} {\sigma'}\) for all well typed types \(A = A'\)

* \(\sigma \circ \tau = \sigma \circ \tau'\) for all well typed substitutions \(\tau = \tau'\).

Prove by mutual induction on the equality of types, terms, and substitutions.

* Take equality \(A = A'\). If this is an instance of \(\star = \star\) then \(\sub \star \rho \equiv \star\) for any \(\rho\), so the result is trivial. If it is instead an instance of \(\arr s B t = \arr {s'} {B'} {t'}\) from \(s = s'\), \(t = t'\), and \(B = B'\). Then by inductive hypothesis we get:

\begin{align*}
\sub A \sigma &= \sub {(\arr s B t)} \sigma\\
&= \arr {\sub s \sigma} {\sub B \sigma} {\sub t \sigma}\\
&= \arr {\sub {s'} {\sigma'}} {\sub {B'} {\sigma'}} {\sub {t'} {\sigma'}}\\
&= \sub {\arr {s'} {B'} {t'}} {\sigma'}\\
&= \sub {A'} {\sigma'}
\end{align*}

* Take equality \(t = t'\). If this is an instance of \(x = x\) then we need that \(\sigma(x) = \sigma'(x)\), which follows from \(\sigma = \sigma'\). If it is an instance of transitivity or symmetry, then we can simply use inductive hypothesis and transitivity or symmetry on the resulting terms. For the structural coherence case we have \(\Coh \Delta B \rho = \Coh \Delta {B'} {\rho'}\) with \(B = B'\) and \(\rho = \rho'\). Then \(\sub t \sigma \equiv \Coh \Delta B {\sigma \circ \rho}\) and \(\sub {t'} {\sigma'} \equiv \Coh \Delta {B'} {\sigma' \circ \rho'}\). Using inductive hypothesis we get that \(\sigma \circ \rho = \sigma' \circ \rho'\) and so we can apply the structural coherence rule to get the required equality.

This leaves the insertion case. Suppose we have \(\Coh \Delta B \rho\) with \(\rho(x) = \Coh \Theta C \tau\) and the equality is \(\Coh \Delta B \rho = \Coh {\insertion \Delta x \Theta} {\sub A {\kappa_{\Delta,x,\Theta}}} {\insertion \rho x \tau} \). When we apply the substitutions we get that \(\sub t \sigma \equiv \Coh \Delta B {\sigma \circ \rho}\) and \(\sub {t'} {\sigma'} \equiv \Coh {\insertion \Delta x \Theta} {\sub B {\kappa_{\Delta,x,\Theta}}} {\sigma' \circ (\insertion \rho x \tau)}\). As \((\sigma \circ \rho) (x) \equiv \Coh \Theta C {\sigma \circ \tau}\), we can certainly apply an insertion to \(\sub t \sigma\) to get \(\Coh {\insertion \Delta x \Theta} {\sub B {\kappa_{\Delta,x,\Theta}}} {\insertion {(\sigma \circ \rho)} x {(\sigma \circ \tau)}}\).

It remains to show modulo structural rules that \(\sigma' \circ (\insertion \rho x \tau) = \insertion {(\sigma \circ \rho)} x {(\sigma \circ \tau)}\). By inductive hypothesis we have that \(\sigma' \circ (\insertion \rho x \tau) = \sigma \circ (\insertion \rho x \tau)\), and the remaining equality is given by <ref>.

* The case for substitutions follows easily from inductive hypothesis.

The support operation is invariant under equality.

\(\Cattsa\) is a \(\Catt\)-based type theory.

We proceed by mutually proving the following statements by induction on the equality proofs.

* For any \(\Gamma = \Gamma'\) we have \(\Gamma \vdash\) if and only if  \(\Gamma' \vdash\).

* For any \(A = A'\) we have that for any \(\Gamma = \Gamma'\) that \(\Gamma \vdash A\) if and only if \(\Gamma' \vdash A'\).

* For any \(\sigma = \sigma'\), for all \(\Gamma = \Gamma'\) and \(\Delta = \Delta'\), \(\Gamma \vdash \sigma : \Delta\) if and only if \(\Gamma' \vdash \sigma' : \Delta'\).

* For any \(t = t'\), for all \(\Gamma = \Gamma'\) and \(A = A'\), \(\Gamma \vdash t : A\) if and only if \(\Gamma' \vdash t' : A'\).

Now we split into cases:

* Suppose we have \(\Gamma = \Gamma'\) and want to prove that \(\Gamma \vdash\) if and only if \(\Gamma' \vdash\). Case splitting on the equality:

* If \(\Gamma = \Gamma'\) is an instance of \(\emptyset = \emptyset\) then the result is trivial.

* Otherwise we have \(\Delta, x : A = \Delta, x : A'\) with \(\Delta = \Delta'\) and \(A = A'\). If \(\Delta, x : A \vdash\) then \(\Delta \vdash\) and \(\Delta \vdash A\). By inductive hypothesis, we have that \(\Delta' \vdash\) and \(\Delta' \vdash A'\) and so \(\Delta', x : A' \vdash\). The other direction is symmetrical.

* Suppose we have \(A = A'\). We want to show for all \(\Gamma = \Gamma'\) that \(\Gamma \vdash A\) if and only if \(\Gamma' \vdash A'\). Case splitting on \(A = A'\).

* If it is a case of \(\star = \star\) then the result is trivially true.

* Otherwise the equality is an instance of \(\arr s A t = \arr {s'} {A'} {t'}\) with \(s = s'\), \(A = A'\), \(t = t'\). As above, the result follows easily from inductive hypothesis.

* Suppose we have \(\sigma = \sigma'\). We want to show for all \(\Gamma = \Gamma'\) and \(\Delta = \Delta'\) that \(\Gamma \vdash \sigma : \Delta\) if and only if \(\Gamma' \vdash \sigma' : \Delta'\): Cases splitting on \(\sigma = \sigma'\):

* If the equality is an instance of \(\langle  \rangle = \langle  \rangle\) then again the result is trivial.

* If the equality is an instance of \(\langle \tau, x \mapsto t \rangle = \langle \tau, x \mapsto t' \rangle\) with \(\tau = \tau'\) and \(t = t'\) and then suppose \(\Gamma \vdash \sigma : \Delta\). Then it must be that \(\Delta \equiv \Theta , x : A\) and so as \(\Delta = \Delta'\), \(\Delta' \equiv \Theta', x : A'\) with \(\Theta = \Theta'\) and \(A = A'\). We further have that \(\Gamma \vdash \tau : \Theta\) and \(\Gamma \vdash t : \sub A \tau\). By <ref>, \(\sub A \tau = \sub {A'} {\tau'}\) and so by inductive hypothesis we have that \(\Gamma' \vdash \tau' : \Theta'\) and \(\Gamma' \vdash t' : \sub {A'} {\tau'}\) and so \(\Gamma' \vdash \sigma' : \Delta'\) as required. The other direction again follows the same argument.

* Suppose we have \(t = t'\). We want to show for all \(\Gamma = \Gamma'\) and \(A = A'\) that \(\Gamma \vdash t : A\) if and only if \(\Gamma' \vdash t' : A'\). Case split on \(t = t'\):

* If it is a case of \(x = x\) then suppose we have \(\Gamma \vdash x : A\). Then this typing rule must be derived from (var') so \(x : B \in \Gamma\) and \(A = B\). Then \(x : B' \in \Gamma\) with \(B = B'\) as \(\Gamma = \Gamma'\) and so as equality is a congruence we have \(A' = A = B = B'\) and so we can apply the (var') rule to get \(\Gamma' \vdash x : A'\). The other direction is symmetrical.

* If it is a case of symmetry, then the result follows directly from inductive hypothesis.

* If it is a case of transitivity, then the result also follows directly from inductive hypothesis.

* If it is from the structural rule on coherences we have \(\Coh \Delta B \sigma = \Coh \Delta {B'} {\sigma'}\) with \(B = B'\) and \(\sigma = \sigma'\). Suppose we have \(\Gamma \vdash \Coh \Delta B \sigma : A\) by the composition rule or coherence rule. In this case we have \(A = \sub B \sigma\), \(\Delta \vdash B\), and \(\Gamma \vdash \sigma : \Delta\). Then by inductive hypothesis we have \(\Delta \vdash B'\) and \(\Gamma' \vdash \sigma' : \Delta\). Further we have \(A' = A = \sub B \sigma = \sub {B'} {\sigma'}\) by equality being a congruence and <ref>. Then, using <ref> and a coherence or composition rule, we get that \(\Gamma' \vdash t' : A'\). The other direction follows similarly.

* The last case is where the equality is an instance of insertion. Here we have \(t \equiv \Coh \Delta B \sigma\) with \(\sigma(x) = \Coh \Theta C \tau\) and \(t' \equiv \Coh {\insertion \Delta x \Theta} {\sub B {\kappa}} {\insertion \sigma x \tau}\).

For the reverse direction we assume that \(\Gamma \vdash t' : A'\). By assumption of insertion we have that \(\Gamma \vdash t : D\) for some type \(D\). Then by inspection of rules we must have that \(D = \sub B \sigma\). Similarly we have that \(A' = \sub {\sub B \kappa} {\insertion \sigma x \tau} = \sub B {(\insertion \sigma x \tau) \circ \kappa} = \sub B \sigma\) and so \(D = A'\).

Conversely assume that \(\Gamma \vdash t : A\). Using inductive hypothesis we get that \(B\) is well typed in \(\Delta\) and \(\sigma\) is well typed from \(\Delta\) to \(\Gamma'\). Then by results in the previous section we have that \(\insertion \Delta x \Theta\) is a pasting context, \(\kappa\) is well typed and so \(\sub B \kappa\) is well typed, and \(\insertion \sigma x \tau\) is a valid substitution from \(\insertion \Delta x \Theta\) to \(\Gamma'\). Therefore \(t'\) can be typed with any type equal to \(\sub {\sub B \kappa} {\insertion \sigma x \tau} = \sub B \sigma\). Now suppose \(A' = A\). Similarly to before we have \(A = \sub B \sigma\) so by \(=\) being a congruence we have \(A' = \sub B \sigma\) and so \(\Gamma' \vdash t' : A'\).

This completes all cases and is sufficient to show what was required.

§ REDUCTION

So far we have given a type theory which models strictly associative infinity categories. Unfortunately, our type theory currently has no way to decide equality and by extension perform type checking. To solve this we introduce a reduction relation, show that it agrees with the definitional equality, and show that it is complete by showing it has strong normalisation and local confluence.

The following rules are admissible for reducing types.

* If \(s \rto s'\):

\[
\arr s A t \rto \arr {s'} A t
\]

* If \(t \rto t'\):

\[
\arr s A t \rto \arr s A {t'}
\]

* If \(A \rto A'\):

\[
\arr s A t \rto \arr s {A'} t
\]

The following rules can be used to reduce substitutions:

* If \(\sigma \rto \sigma'\):
\(\langle \sigma, t \rangle \rto \langle \sigma', t \rangle\)

* If \(t \rto t'\):
\(\langle \sigma, t \rangle \rto \langle \sigma, t' \rangle\)

This effectively allows any term in the substitution to be reduced.

The following rules can be used to reduce terms:

* (Insertion): If \(x\) is locally maximal in \(\Delta\) and \(\sigma(x)\) is the unbiased composite \(\Coh \Theta B \tau\) with the branching height of \(x\) being less than or equal to the linear height of \(\Theta\) then:

\[\Coh \Delta A \sigma \rto \Coh {\insertion \Delta x \Theta} {\sub A {\kappa_{\Delta,x,\Theta}}} {\insertion \sigma x \tau} \]

* (Cell reduction): The type of a coherence can be reduced, so if \(A \rto A'\) then:

\[\Coh {\Delta} A \sigma \rto \Coh {\Delta} {A'} \sigma\]

* (Argument reduction): The arguments to a coherence can be reduced, so if \(\sigma \rto \sigma'\) then:

\[\Coh \Delta A \sigma \rto \Coh \Delta A {\sigma'}\]

For all terms \(t \rto t'\), types \(A \rto A'\), and substitutions \(\sigma \rto \sigma'\), and another substitution \(\tau\), then \(\sub t \tau \rto \sub {t'} \tau\), \(\sub A \tau \rto \sub {A'} \tau\) and \(\tau \circ \sigma \rto \tau \circ \sigma'\).

Proceed by mutual induction on \(t\), \(A\), and \(\sigma\).

* For substitutions \(\sigma = \langle t_0, \dots, t_n \rangle\), we have \(\sigma \rto \sigma'\) and therefore there must be some \(i\) with \(t_i \rto t_i'\) and \(\sigma' = \langle t_0,\dots,t_i',\dots,t_n \rangle\). Further, \(\tau \circ \sigma = \langle \sub {t_0} \tau, \dots, \sub {t_n} \tau \rangle\) and \(\tau \circ \sigma' = \langle \sub {t_0} \tau, \dots, \sub {t_i'} \tau, \dots, \sub {t_n} \tau \rangle\) and so by inductive hypothesis \(\sub {t_i} \tau \rto \sub {t_i'} \tau\) and so \(\tau \circ \sigma \rto \tau \circ \sigma'\).

* For types we get a proof similar to above where we apply the inductive hypothesis to some subterm.

* For terms \(t\), we note that \(t\) cannot be a variable as variables do not reduce. Therefore \(t \equiv \Coh \Delta A \sigma\) and \(\sub t \tau \equiv \Coh \Delta A {\tau \circ \sigma}\). Now we case split on the possible reductions of \(t\).

* Cell reduction: The type \(A\) is unaffected by substitution so this remains unchanged.

* Argument reduction: Follows from inductive hypothesis.

* Insertion: Suppose \(t \rto t'\) is an insertion along \(x\) and \(\sigma(x) \equiv \Coh \Theta B \rho\). Then \((\tau \circ \sigma) (x) \equiv \Coh \Theta B {\tau \circ \rho}\) and so \(\sub t \tau\) admits an insertion. We must have \(t' \equiv \Coh {\insertion \Delta x \Theta} {\sub B {\kappa}} {\insertion \sigma x \rho}\) and \(\sub t \tau\) reduces by insertion to \(\Coh {\insertion \Delta x \Theta} {\sub B {\kappa}} {\insertion {(\tau \circ \sigma)} x {(\tau \circ \rho)}}\). It remains to show that \(\tau \circ {(\insertion \sigma x \rho)} \equiv \insertion {(\tau \circ \sigma)} x {(\tau \circ \rho)}\) but this is given by <ref>.

We end this section by showing that reduction agrees with equality in the following way.

Let \(\rto'\) be the reduction \(\rto\) restricted to terms that are well typed, and \(\rto'_{\mathsf{rts}}\) be the reflexive transitive symmetric closure of this reduction.

On valid terms, types and substitutions, the equality relation \(=\) agrees with \(\rto'_{\mathsf {rts}}\).

It is clear that if \(p \rto'_{\mathsf{rts}} q\) then \(p = q\). Therefore we only need to prove the other direction. As in <cit.>, we define a term \(p\) to be conservative if for all \(q\) with \(p = q\), we have \(p \rto'_{\mathsf{rts}} q\). The only case that doesn't follow almost immediately from inductive hypothesis is the case where \(p = q\) is by insertion. Therefore suppose \(p \equiv \Coh \Delta A \sigma\) and \(\sigma(x) = \Coh \Theta U \tau\) and \(q \equiv \Coh {\insertion \Delta x \Theta} {\sub A \iota} {\insertion \sigma x \tau}\). Then by induction on subterms we have that \(\sigma(x) \rto'_{\mathsf{rts}} \Coh \Theta U \tau\) and so \(p \rto'_{\mathsf{rts}} \Coh \Delta A {\sigma'} \rto' q\) where \(\sigma'\) is \(\sigma\) with \(\sigma(x)\) replaced with \(\Coh \Theta U \tau\).

§.§ Termination

In this section we prove termination of the reduction scheme presented above. To do this we will map each term to an ordinal, show that all reductions reduce this ordinal.

The natural sum of ordinals \(\alpha \+ \beta\) is defined by simultaneous induction on \(\alpha\) and \(\beta\) by:

0  0        = 0

α β      = sup_
α' < α
β' < β

{ S(α β'), S(α'  β) }

The natural sum of ordinals is associative, commutative, and strictly monotone in both arguments.

See <cit.>.

Define the syntactic depth \(\sd\) of substitutions, typed, and terms by mutual induction:

* For substitutions we have:

\[\sd(\langle t_0, \dots, t_n \rangle) = \bighash_{i=0}^n t_i\]

* For types we have \(\sd(\star) = 0\) and:

\[\sd(\arr s A t) = \sd(s) \+ \sd(A) \+ \sd(t)\]

* For variables \(x\), \(\sd(x) = 0\).

* For coherences define:

\[\sd(\Coh \Delta A \sigma) = \omega^{\dim(A)} \+ \sd(A) \+ \sd(\sigma)\]

For terms \(t \rto t'\), \(\sd(t) > \sd(t')\), for types \(A \rto A'\), \(\sd(A) > \sd(A')\), and for substitutions \(\sigma \rto \sigma'\), \(\sd(\sigma) > \sd(\sigma')\).

By mutual induction on term reductions \(t \rto t'\), type reductions \(A \rto A'\) and substitution reductions \(\sigma \rto \sigma'\):

* For substitutions, if \(\sigma \rto \sigma'\) then suppose \(\sigma = \langle t_0, \dots, t_n \rangle\) and \(\sigma' = \langle t_0', \dots, t_n' \rangle\). Then for some \(i\) we must have \(t_i \rto t_i'\) and \(t_k = t_k'\) for \(k \neq i\). By inductive hypothesis \(\sd(t_i) > \sd(t_i')\) and so \(\sd(\sigma) > \sd(\sigma')\).

* For types, \(\star\) admits no reductions so suppose \(A \equiv \arr s B t\). If \(A' \equiv \arr {s'} B t\) where \(s \rto s'\) then by inductive hypothesis \(\sd(s) > \sd(s')\) and so \(\sd(A) > \sd(A')\). The cases where \(A' \equiv \arr s {B'} t\) and \(A' \equiv \arr s B {t'}\) follow similarly.

* For term reductions \(t \rto t'\) we first split on the reduction. Note that as variables do not reduce, we must have that \(t \equiv \Coh \Delta A \sigma\).

* Argument reduction: If \(t \rto t'\) is an argument reduction then \(t' \equiv \Coh \Delta A {\sigma'}\) where \(\sigma \rto \sigma'\). By inductive hypothesis, \(\sd(\sigma) > \sd(\sigma')\) and so \(sd(t) > \sd(t')\).

* Cell reduction: If \(t \rto t'\) is a cell reduction then we have \(t' \equiv \Coh \Delta {A'} \sigma\) with \(A \rto A'\). By inductive hypothesis \(\sd(A) > \sd(A')\) and so \(\sd(t) \geq \sd(t')\).

* Insertion: If \(t \rto t'\) is an insertion along a variable \(x\) then let \(\sigma(x) \equiv \Coh \Theta B \tau\). Now let \(\mu \equiv \insertion \sigma x \tau\) and let \(I \equiv \insertion \Delta x \Theta\). Then:

\begin{align*}
\omega^{\dim(A)} \+ \sd(\mu) &= \omega^{\dim(A)} \+ \bighash_{y \in \Var(I)} \sd(\mu(y))\\
&= \omega^{\dim(A)} \+ \bighash_{y \in \Var(I) \cap \Var(\Theta)} \sd(\mu(y)) \+ \bighash_{y \in \Var(I) \cap \Var(\Delta)} \sd(\mu(y)) \\
&= \omega^{\dim(A)} \+ \bighash_{y \in \Var(\Theta)} \sd(\tau(y)) \+ \bighash_{y \in \Var(I) \cap \Var(\Delta)} \sd(\sigma(y))\\
&= \omega^{\dim(A)} \+ \sd(\tau) \+ \bighash_{y \in \Var(I) \cap \Var(\Delta)} \sd(\sigma(y))\\
&\geq \sd(\sigma(x)) \+ \bighash_{y \in \Var(I) \cap \Var(\Delta)} \sd(\sigma(y))\\
&= \bighash_{y \in (\Var(I) \cup \{x\}) \cap \Var(\Delta)} \sd(\sigma(x))\\
&\leq \bighash_{y \in \Var(\Delta)} \sd(\sigma(y))\\
&= \sd(\sigma)
\end{align*}

Then by assumption, \(t\) is not a coherence on a disc, and so is not an identity. Therefore:

\begin{align*}
\sd(t) &=  \omega^{\dim(t)} \+ \sd(A) \+ \sd(\sigma)\\
&\geq \omega^{\dim(t)} \+ \sd(\sigma) \\
&\geq \omega^{\dim(t)} \+ \omega^{\dim(t)} \+ \sd(\insertion \sigma x \tau)\\
&> \omega^{\dim(t)} \+ \sd(\sub A \kappa) \+ \sd((\insertion \sigma x \tau)) \\
&= \sd(t')
\end{align*}

where \(\omega^{\dim(t)} > \sd(\sub A \kappa)\) due to dimension.

This covers all cases, and so completes the proof.

The reduction \(\rto\) is strongly normalising on types, terms, and substitutions.

Suppose an infinite reduction sequence \(t_0 \rto t_1 \rto \dots\) exists. Then by <ref>, \(sd(t_0) > \sd(t_1) > \dots\) is an infinitely decreasing sequence of ordinals, which cannot exist.

§.§ Confluence

In this section we show that \(\rto'\) is locally confluent, which implies along with <ref> that \(\rto'\) is globally confluent and hence complete.

Mutually define a term \(t\) being regular and its regular height, an extended natural number as follows:

* If \(t\) is a variable then it is regular and its regular height is \(\infty\)

* If \(t \equiv \Coh \Delta U \sigma\), then \(t\) is regular if and only if \(\Delta\) is not a disk, \(U\) is the unbiased type over \(\Delta\), every term in \(\sigma\) is regular, and for all \(x \in \LM(\Delta)\), the branching height of \(x\) is less than the regular height of \(\sigma(x)\). If \(t\) is regular, then its regular height is given by the linear height of \(\Delta\).

If \(I,\iota_i,\iota_e\) is an insertion of \((\Theta,B)\) into \((\Delta,x)\), with \(U\) is the unbiased type over \(\Delta\) and \(B\) is the unbiased type over \(\Theta\), then all terms contained in \(\sub U {\iota_e}\) are regular, as all the terms in \(U\) are unbiased composites of variables, and we substitute in unbiased composites which satisfy the height condition from the conditions of insertion.

Further note that if the support of a regular term is a disc, then it must be a variable, as any unbiased composite will have multiple locally maximal variables in its support.

If \(t\) is a regular term over a pasting diagram, then it reduces to the unbiased composite of its support.

Proceed by mutual reduction on dimension and subterms. The hypothesis on dimension tells us that if a regular term undergoes an insertion, then it reduces to another regular term, (in other words the type reduces to the unbiased type). Further, we must have that the regular height of the new reduced term is at least the regular height of the original term. Therefore take an arbitrary term \(t\), and repeatedly perform insertions followed by making everything unbiased. By termination, we will eventually get term \(t'\) with \(t \rto t'\) and \(t'\) having no more possible insertions.

If \(t'\) is a variable then we are done. Otherwise, \(t'\) is an unbiased composition. By construction, \(t'\) does not admit any insertions, so all locally maximal dimensional arguments must be variables (or \(t'\) would not be regular). Now suppose there is an argument \(x\) is not a variable. Then there is such an argument \(u\) with maximal dimension. This can not be locally maximal so it is the source or target of a variable. Then its support must be a disc, but this contradicts its regularity.

If \(t\) is an unbiased composite and admits an insertion, then the resulting term reduces to an unbiased composite.

The reduction \(\rto'\) is locally confluent. In other words if \(a\), \(b\), and \(c\) are valid terms, with \(a \rto b\) and \(a \rto c\) then there exists valid \(u\) with \(b \rto_{\mathsf{rt}} u\) and \(c \rto_{\mathsf{rt}} u\).

Proceed by mutual induction on subterms and dimension. By induction on dimension we have that \(\rto\) is locally confluent on \(m\)-dimensional terms for \(m < \dim(a)\) and so is globally confluent (for dimension \(m\)). Further, as \(\rto\) is terminating (by <ref>) and agrees with equality (by <ref>), we have that any equal terms with dimension less than \(\dim(a)\) have a common normal form. It also holds that if \(s =_m t\) for some \(m < \dim(a)\), then there is \(u\) with \(s \rto_{\mathsf{rt}} u\) and \(t \rto_{\mathsf{rt}} u\).

Suppose \(a \rto b\) and \(a \rto c\). Split into cases.

* Both are insertions. If they are insertions on the same variable, then \(b \equiv c\) and we are done. Otherwise let \(a \equiv \Coh \Gamma A \sigma\), and suppose \(b\) is an insertion along \(x\) with \(\sigma(x) \equiv \Coh \Delta B \tau\) and \(c\) is an insertion along \(y\) with \(\sigma(y) \equiv \Coh \Theta C \mu\). Further we must have that \(x\) and \(y\) are locally maximal, so in particular are not in each other's support.

\[\begin{tikzcd}
& {D^n} & \Delta \\
{D^m} & \Gamma & {\insertion \Gamma x \Delta} \\
\Theta
\arrow["\overline{x}", from=1-2, to=2-2]
\arrow["{\overline{\Coh \Delta B \id}}", from=1-2, to=1-3]
\arrow[from=2-2, to=2-3]
\arrow[from=1-3, to=2-3]
\arrow["\overline{y}", from=2-1, to=2-2]
\arrow["{\overline{\Coh \Theta C \id}}"', from=2-1, to=3-1]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=180}, draw=none, from=2-3, to=1-2]
\end{tikzcd}\]

In the diagram above we construct the insertion along \(x\). Now we can notice that the composite \(D^m \overset{y}{\to} \Gamma \to \insertion \Gamma x \Delta\) is just the substitution \(\overline{y}\), and so we can perform another insertion (as the branching height of \(y\) must be the same in \(\Gamma\) and \(\insertion \Gamma x \Delta\)). We then get the following diagram:

\[\begin{tikzcd}
& {D^n} & \Delta \\
{D^m} & \Gamma & {\insertion \Gamma x \Delta} \\
\\
\Theta && {\insertion {(\insertion \Gamma x \Delta)} y \Theta}
\arrow["\overline{x}", from=1-2, to=2-2]
\arrow["{\overline{\Coh \Delta B \id}}", from=1-2, to=1-3]
\arrow[from=2-2, to=2-3]
\arrow[from=1-3, to=2-3]
\arrow["\overline{y}", from=2-1, to=2-2]
\arrow["{\overline{\Coh \Theta C \id}}"', from=2-1, to=4-1]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=180}, draw=none, from=2-3, to=1-2]
\arrow[from=2-3, to=4-3]
\arrow[from=4-1, to=4-3]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=180}, draw=none, from=4-3, to=2-1]
\end{tikzcd}\]

and therefore \(\insertion {(\insertion \Gamma x \Delta)} y \Theta\) is the colimit of:

\[\begin{tikzcd}
& {D^n} & \Delta \\
{D^m} & \Gamma \\
\Theta
\arrow["\overline{x}", from=1-2, to=2-2]
\arrow["{\overline{\Coh \Delta B \id}}", from=1-2, to=1-3]
\arrow["\overline{y}", from=2-1, to=2-2]
\arrow["{\overline{\Coh \Theta C \id}}"', from=2-1, to=3-1]
\end{tikzcd}\]

Similarly, \(\insertion {(\insertion \Gamma y \Theta)} x \Delta\) is a colimit of the same diagram and so is equal. Further, it can easily be checked that \(\insertion {(\insertion \sigma y \mu)} x \tau\) and \(\insertion {(\insertion \sigma x \tau)} y \mu\) both satisfy the necessary equations to be equal by uniqueness of the map out of a colimit. It is then simple to check that the maximal dimension parts of these two substitutions are actually definitionally equal by case analysis and so we get

\begin{align*}
b &\rto \Coh {\insertion {(\insertion \Gamma x \Delta)} y \Theta} {\sub A {\kappa_{(\insertion \Gamma x \Delta), y , \Theta} \circ \kappa_{\Delta, x, \Gamma}}} {\insertion {(\insertion \sigma x \tau)} y \mu} \\
&=_{\dim(a)} \Coh {\insertion {(\insertion \Gamma y \Theta)} x \Delta} {\sub A {\kappa_{(\insertion \Gamma y \Theta), x, \Delta} \circ \kappa_{\Theta, y, \Gamma}}} {\insertion {(\insertion \sigma y \mu)} x \tau}\\
&\leftsquigarrow c
\end{align*}

which gives us a way to construct a suitable \(u\) by the comment at the start of the proof.

* Now suppose both reductions are argument reductions. If these occur on different arguments, we simply apply both to get a suitable \(u\), and if they are the same argument then we use the inductive hypothesis on subterms.

* Now suppose \(a \rto b\) is an insertion and \(a \rto c\) is an argument reduction. The only case which is hard is when the insertion and argument reduction are along the same variable. Therefore we can assume we are in the case where \(a \equiv \Coh \Gamma A \sigma\) and \(\sigma(x) \equiv \Coh \Delta B \tau\) and \(\tau(y) \equiv \Coh \Theta C \mu\).

Firstly assume that \(\Delta\) is a disc context. Then \(\sigma(x)\) just reduces to \(\tau(y)\) by performing the argument insertion first. If instead the head insertion is performed first then the head pasting diagram is unchanged (up to variable renaming) but the arguments can be changed. We see that \(x\) must be sent to \(\tau(y)\). Therefore \(b =_{\dim(x)} c\) and so we can find suitable \(u\) as before.

Now we assume \(\Delta\) is not a disc context. First consider the case where the insertion is done first. Then we get the following diagram:

\[\begin{tikzcd}
& {D^n} & \Gamma \\
{D^m} & \Delta & {\insertion \Gamma x \Delta} \\
\\
\Theta && {\insertion {(\insertion \Gamma x \Delta)} y \Theta}
\arrow["\overline{x}", from=1-2, to=1-3]
\arrow["\overline{y}", from=2-1, to=2-2]
\arrow[from=2-2, to=2-3]
\arrow[from=1-3, to=2-3]
\arrow["{\overline{\Coh \Delta B \id}}"', from=1-2, to=2-2]
\arrow["{\overline{\Coh \Theta C \id}}"', from=2-1, to=4-1]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=180}, draw=none, from=2-3, to=1-2]
\arrow[from=4-1, to=4-3]
\arrow[from=2-3, to=4-3]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=180}, draw=none, from=4-3, to=2-1]
\end{tikzcd}\]

where we can perform the second insertion as the composite \(D^m \overset y \to \Delta \to \insertion \Gamma x \Delta\) is just the variable \(y\) (as \(\Delta \to \insertion \Gamma x \Delta\) is variable to variable) and \(y\) has the same branching height in \(\Delta\) and \(\insertion \Gamma x \Delta\) as \(\Delta\) is not a disc context.

Now consider first applying the argument insertion to get this diagram:

\[\begin{tikzcd}
& {D^n} & \Gamma \\
{D^m} & \Delta \\
\Theta & {\insertion \Delta y \Theta}
\arrow["\overline{x}", from=1-2, to=1-3]
\arrow["\overline{y}", from=2-1, to=2-2]
\arrow["{\overline{\Coh \Delta B \id}}"', from=1-2, to=2-2]
\arrow["{\overline{\Coh \Theta C \id}}"', from=2-1, to=3-1]
\arrow[from=2-2, to=3-2]
\arrow[from=3-1, to=3-2]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=180}, draw=none, from=3-2, to=2-1]
\end{tikzcd}\]

Now note that there is a second map from \(D^n\) to \(\insertion \Delta y \Theta\) given by \(\Coh {\insertion \Delta y \Theta} U \id\) where \(U\) is the unbiased type of \(\insertion \Delta y \Theta\) and by an insertion and <ref> these are equal. As \(\Delta\) is not a disc context, the linear height of \(\insertion \Delta y \Theta\) is at least as high as \(\Delta\) and so we can complete the second insertion to get:

\[\begin{tikzcd}
& {D^n} && \Gamma \\
{D^m} & \Delta \\
\Theta & {\insertion \Delta y \Theta} && {\insertion \Gamma x {(\insertion \Delta y \Theta)}}
\arrow["\overline{x}", from=1-2, to=1-4]
\arrow["\overline{y}", from=2-1, to=2-2]
\arrow["{\overline{\Coh \Delta B \id}}"', from=1-2, to=2-2]
\arrow["{\overline{\Coh \Theta C \id}}"', from=2-1, to=3-1]
\arrow[from=2-2, to=3-2]
\arrow[from=3-1, to=3-2]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=180}, draw=none, from=3-2, to=2-1]
\arrow[""{name=0, anchor=center, inner sep=0}, "{\overline{\Coh {\insertion \Delta y \Theta} U \id}}", curve={height=-30pt}, from=1-2, to=3-2]
\arrow[from=1-4, to=3-4]
\arrow[from=3-2, to=3-4]
\arrow["{=}"{description}, Rightarrow, draw=none, from=2-2, to=0]
\end{tikzcd}\]

Then as before, both of these insertions arise from the same colimit and we can apply the same reasoning as the insertion-insertion case, which completes the proof.

§ TYPECHECKING

Using the reduction in the previous section, we can show that equality and typechecking are decidable.

Define the normalisation function \(N\) as a function taking terms to terms, types to types, and substitutions to substitutions, given by repeatedly applying the innermost leftmost reduction until a normal form is found.

If \(s\) and \(t\) are valid terms, then \(s = t\) if and only if \(N(s) \equiv N(t)\). A similar result holds for valid typed \(A\) and \(B\), and valid substitutions \(\sigma\) and \(\tau\).

This gives us a way to decide equality between terms which are valid, as we can simply compute the normalisation of each term and checking syntactic equality is clearly decidable. We can now show how this can be used to perform decidable typechecking.

Typechecking on terms, types, substitutions, and contexts is decidable.

We work by mutual induction on terms, types, substitutions, and contexts.

* For typechecking whether \(\Gamma \vdash t : A\), we split into cases:

* If \(t\) is a variable, then we check whether \(t \in \Gamma\). If it is not, then \(t\) is not valid in \(\Gamma\). If \(t : B\) in \(\Gamma\) then we just need to check if \(A = B\).

* If \(t \equiv \Coh \Delta B \sigma\), then for \(t\) to be valid, it is necessary that \(\Gamma \vdash \sigma : \Delta\), \(\Delta \vdash_p\), and \(\Delta \vdash B\). It can be easily checked that \(\Delta\) is a pasting diagram, and the other two can be checked by inductive hypothesis. We then need to further check that the support conditions hold for either the coherence or composition rule. Finally, if all other conditions hold then \(\Gamma \vdash t : A\) if and only if \(A = \sub B \sigma\).

* For typechecking \(\Gamma \vdash A\), if \(A \equiv \star\) then \(A\) is valid, and if \(A \equiv \arr s B t\), then \(A\) is valid if and only if \(\Gamma \vdash B\), \(\Gamma \vdash s : B\), and \(\Gamma \vdash t : B\), all of which can be checked by inductive hypothesis.

* Typechecking for substitutions similarly follows from inductive hypothesis.

* The empty context is always valid, and \(\Gamma, x : A\) can be checked by checking whether \(\Gamma \vdash\) and \(\Gamma \vdash A\).

This gives us a fully decidable procedure for typechecking. It can also be noted that we can extract a type inference algorithm for terms from this proof.

Talk about implementation?

Missing 'biblatex' package
The bibliography requires the 'biblatex' package.

Institut Polytechnique de Paris

titleA type theoretic approach to weak \(\omega\)-categories and related higher structures
Type theory ; Higher categories ; Category theory ; Pasting schemes ; Semantics ; Homotopy type theory ; Théorie des types ; Catégories supérieures ; Théorie des catégories ; Diagrammes de compositions ; Sémantique ; Théorie homotopique des types

titleGlobular weak \(\omega\)-categories as models of a type theory
nique.fr/ tbenjamin/articles/publications/models.pdf

abstractWe define novel fully combinatorial models of higher categories. Our definitions are based on a connection of higher categories to "directed spaces". Directed spaces are locally modelled on manifold diagrams, which are stratifications of the n-cube such that strata are transversal to the flag foliation of the n-cube. The first part of this thesis develops a combinatorial model for manifold diagrams called singular n-cubes. In the second part we apply this model to build our notions of higher categories. Singular n-cubes are "directed triangulations" of space together with a decomposition into a collection of subspaces or strata. Singular n-cubes can be naturally organised into two categories. The first, whose morphisms are bundles themselves, is used for the inductive definition of singular (n+1)-cubes. The second, whose morphisms are "open" base changes, admits an (epi,mono) factorisation system. Monomorphisms will be called embeddings of cubes. Epimorphisms will be called collapses and describe how triangulations can be coarsened. Each cube has a unique coarsest triangulation called its normal form. The existence of normal forms makes the equality relation of (combinatorially represented) manifold diagrams decidable. As the main application of the resulting combinatorial framework for manifold diagrams, we give algebraic definitions of various notions of higher categories. Namely, we define associative n-categories, presented associative n-categories and presented associative n-groupoids. All three notions will have strict units and associators; the only weak coherences are homotopies, but we develop a mechanism for recovering the usual coherence data of weak n-categories, such as associators and pentagonators and their higher analogues. This will motivate the conjecture that the theory of associative higher categories is equivalent to its fully weak counterpart.
titleAssociative $n$-categories

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

abstractWe 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.
titleA Type Theory for Strictly Unital $\infty$-Categories
given=A. J.,

United States

American Mathematical Society

abstractThis work defines the concept of tricategory as the natural 3-dimensional generalization of bicategory. Trihomomorphism and triequivalence for tricategories are also defined so as to extend the concepts of homomorphism and biequivalence for bicategories. The main theorem is a coherence theorem for tricategories which asserts the existence of a triequivalence between each tricategory and some V-category, where V is the category of 2-categories equipped with the strong tenser product of J. W. Gray. Further, it is shown that while not every tricategory is triequivalent to a 3-category, every tricategory that is locally a 2-category and whose composition is a 2-functor is triequivalent to a 3-category. The work has applications to cohomology theory, homotopy theory, bicategory enriched categories, and bicategories with extra structure.
titleCoherence for tricategories
TRICATEGORY,MONOIDAL BICATEGORY,GRAY-CATEGORY,ALGEBRAIC HOMOTOPY 3-TYPE,LAX FUNCTOR OF TRICATEGORIES,TRIHOMOMORPHISM,TRIEQUIVALENCE,CUBICAL FUNCTOR,CUBICAL TRICATEGORY,PREREPRESENTATION,BICATEGORIES,CATEGORIES

titleWeak Units and Homotopy 3-types

abstractA concrete computation – twelve slidings with sixteen tiles – reveals that certain commutativity phenomena occur in every double semigroup. This can be seen as a sort of Eckmann-Hilton argument, but it does not use units. The result implies in particular that all cancellative double semigroups and all inverse double semigroups are commutative. Stepping up one dimension, the result is used to prove that all strictly associative two-fold monoidal categories (with weak units) are degenerate symmetric. In particular, strictly associative one-object, one-arrow 3-groupoids (with weak units) cannot realise all simply-connected homotopy 3-types.
titleNote on Commutativity in Double Semigroups and Two-Fold Monoidal Categories

titleA Survey of Definitions of n-Category

journaltitleMathematical Logic Quarterly
titleAn Infinite Natural Sum

journaltitlearXiv preprint arXiv:1009.2331
titleGrothendieck $\infty$-groupoids, and still another definition of $\infty$-categories

journaltitlearXiv preprint arXiv:1902.03831
titleHigh-level methods for homotopy construction in associative $ n $-categories

abstractWe look at strict $n$-groupoids and show that if $\Re$ is any realization functor from the category of strict $n$-groupoids to the category of spaces satisfying a minimal property of compatibility with homotopy groups, then there is no strict $n$-groupoid $G$ such that $\Re (G)$ is the $n$-type of $S^2$ (for $n\geq 3$). At the end we speculate on how one might fix this problem by introducing a notion of “snucategory”, a strictly associative $n$-category with only weak units.
titleHomotopy Types of Strict 3-groupoids


:
ML4H Extended Abstract Arxiv Index 2020 2020 Machine Learning for Health
(ML4H) 2020

# Natural Language Processing to Detect Cognitive Concerns in Electronic
Health Records Using Deep Learning

Zhuoqiao Hong1 Authors contributed equally Colin G. Magdamo11footnotemark: 11
Yi-han Sheu11footnotemark: 11 Prathamesh Mohite1 Ayush Noori1 Elissa M. Ye1
Wendong Ge1 Haoqi Sun1 Laura Brenner1 Gregory Robbins1 Shibani Mukerji1 Sahar
Zafar1 Nicole Benson1 Lidia Moura1 John Hsu1 Bradley T. Hyman1 Michael B.
Westover1 Deborah Blacker1 Sudeshna Das1
1{zhong1, cmagdamo, ysheu, pmohite, anoori1, emye, wendong.ge, hsun8,
lnbrenner, grobbins, smukerji, sfzafar, nbenson, lidia.moura, john.hsu,
bhyman, mwestover, dblacker, sdas5} @mgh.harvard.edu  Massachusetts General
Hospital Boston  MA

###### Abstract

Dementia is under-recognized in the community, under-diagnosed by healthcare
professionals, and under-coded in claims data. Information on cognitive
dysfunction, however, is often found in unstructured clinician notes within
medical records but manual review by experts is time consuming and often prone
to errors. Automated mining of these notes presents a potential opportunity to
label patients with cognitive concerns who could benefit from an evaluation or
be referred to specialist care. In order to identify patients with cognitive
concerns in electronic medical records, we applied natural language processing
(NLP) algorithms and compared model performance to a baseline model that used
structured diagnosis codes and medication data only. An attention-based deep
learning model outperformed the baseline model and other simpler models.

###### keywords:

NLP, EHR, Dementia

##  1 Introduction

Early detection of dementia is important for improving clinical outcomes and
management of dementia, as well as for lifestyle, financial, and future
planning for patients and their caregivers (Robinson et al., 2015; Borson et
al., 2013). Yet, dementia is not formally diagnosed or coded in claims for
over 50% of older adults living with probable dementia (Amjad et al., 2018;
Alzheimer’s Association, 2019). Tools that screen medical records for warning
signs and present the digested information to providers may prove to be an
important step for early intervention. In this study, we aim to use NLP to
detect signs of cognitive dysfunction from clinician notes in electronic
health records (EHR) by applying deep learning techniques that have not been
hitherto applied to this problem. We present an attention-based transformer
model that allows for long text sequences to reveal signs of cognitive
concerns and compare its performance to baseline models.

##  2 Related Work

Prior works have used pattern based text-analytics to detect dementia in
electronic health records. Dementia detection using NLP on provider notes has
been applied to a cohort of acute-care EHRs of hip and stroke fracture
patients (Gilmore-Bykovskyi et al., 2018); a sample of patients enrolled in
the UCLA Alzheimer’s and Dementia Care (ADC) program (Reuben et al., 2017);
and a group of patients who had a formal cognitive evaluation by the Mayo
Clinic Study of Aging and were hospitalized at their institution (Amra et al.,
2017). These studies demonstrated that the incorporation of NLP on EHR notes
improves sensitivity of dementia detection. The current work uses deep
learning based NLP, which has achieved numerous breakthroughs when applied to
general text thanks to the use of word embeddings and attention-based models
(Vaswani et al., 2017; Mikolov et al., 2013; Pennington et al., 2014; Peters
et al., 2018; Devlin et al., 2018), while it has had limited application on
healthcare data. Our work builds upon the idea in (Sheu, 2019), where a deep-
learning based model was applied to classify the outcome for treatment of
depression, a phenotype also not captured well by structured data or term-
based NLP, therefore motivating the use of deep learning techniques.

##  3 Datasets and Preprocessing

#### Datasets

Our gold-standard dataset consisted of 1K randomly sampled patients at Mass
General Brigham (MGB) HealthCare (formerly Partner’s Healthcare, comprising
two major academic hospitals, community hospitals, and community health
centers in the Boston area). Each patient’s EHR record between 01/01/2018 –
12/31/2018 was reviewed by an expert clinician (neurologist, psychiatrist, or
geriatric psychiatrist) to label patients with presence or absence of any
cognitive concerns (signs of dementia).

#### Data Preprocessing

For each patient in the gold-standard dataset, we extracted the diagnosis,
medication history, and progress notes from the window between 01/01/2018 –
12/31/2018. We flagged all medications related to cognitive concern
(Galantamine, Donepezil, Rivastigmine, Memantine) as well as all International
Classification of Diseases (ICD) diagnoses pertaining to cognitive concern
(ICD 9 codes: 290.X, 294.X, 331.X, 780.93; ICD 10 codes: G30.X and G31.X). For
each patient, we added the number of records pertaining to the medications of
interest and the number of ICD codes of interest, yielding two features
designed to capture the presence of cognitive concerns in the structured data.
We filtered for patients that had progress notes. Several preprocessing steps
were involved to trim the notes to reduce noise, and note length was decreased
by 50% after these steps, details of which are described in apd:app6. The
preprocessed notes were used as input for all three models that use notes as
input. For the model based on regular expression matches, we constructed 15
categories of keywords (apd:app1). Each category contained multiple regular
expressions that were then flagged within our filtered set of notes. We then
added the number of pattern matches per patient per category across all notes,
resulting in 15 features per patient.

The final dataset of 767 patients was randomly split between train (90%) and
hold-out test (10%) sets. Validation datasets were split within the train set
using different methods for the various models as described in the Methodology
section. tab:example-booktabs shows the demographics of the patients in the
training and test sets.

tab:example-booktabs  Dataset Age (Mean and SD) % Female Cognitive Concern (N)
Train/Val (N = 690) 81.2 (7.4) 58.2% 308 (44.64%) Test (N = 77) 80.19 (6.79)
54.5% 34 (44.16%)

Table 1: Demographics of Train/Val and Test Sets

##  4 Methodology

We built three models and compared the performance to the baseline model.

#### (1) Baseline Model

In model 1, we performed a regularized logistic regression where the cognitive
concern label was regressed on counts of medications and ICD codes related to
cognitive concern. We used the glmnet package (Friedman et al., 2010) in R and
performed L1 regularization. The lambda value in our regularization penalty
was selected via 10-fold cross validation (CV), with the optimal lambda chosen
to maximize the average area under the Receiver Operator Characteristic (ROC)
curve across folds.

#### (2) Logistic Regression with Regular Expression Counts

In model 2, we again utilized regularized logistic regression. We regressed
the cognitive concern label against the 15 features corresponding to counts of
the 15 regular expression categories per patient. We similarly used L1
regularization and 10-fold CV to choose our lambda value.

#### (3) Logistic Regression with TF-IDF Vectors

In model 3, we performed a TF-IDF (term frequency–inverse document frequency)
vectorization to select features based on the term’s correlation coefficient,
and performed a regularized logistic regression using the cognitive concern
label as the outcome. We used different correlation coefficients as thresholds
to select word features, and iterated with different lambda values on a
validation dataset (10% from train dataset) to determine our best lambda value
and the specific correlation cutoff threshold.

#### (4) Transformer Based Sequence Classification Language Model

In model 4, we utilized a pre-trained language model with an attention
mechanism, Longformer (Beltagy et al., 2020), which deploys a modified self-
attention mechanism whose complexity scales linearly with sequence length and
thus allows accommodation of longer sequences. The model was initialized with
pre-trained parameters and was later fine-tuned with our labeled training
dataset. Hyperparameters were tuned on a held out validation dataset (10% from
the train dataset) for the cognitive concern classification task.

##  5 Experiments and Results

###  5.1 Description of Computational Experiments

In model 4 with Longformer (model diagram is shown in apd:app4), we utilized
the implementation in the Huggingface Transformer (Wolf et al., 2019) and
Simpletransformers packages (Rajapakse, 2020). After text preprocessing, input
texts were tokenized with the default tokenizer and converted to embeddings.
Due to the limitation of sequence lengths of Longformer, we used the “sliding
windows” option available in the Simpletransformers package to automatically
slice the input text into windows of 4096 tokens, with 20% overlapping content
between windows _i_ and _i+1_. We used the Adam optimizer (Kingma and Ba,
2014) and tuned the model with an initial learning rate of 7.09e-6, Epsilon
value of 1e-9, and 4 training epochs. Classification of each window was
aggregated (mode) to obtain patient level class assignments. All performance
metrics below are based on patient level class assignments.

tab:performance  Model AUC Accuracy FP FN Sensitivity Specificity PPV NPV
Model 1 0.79 0.82 0 14 0.59 1.00 1.00 0.75 Model 2 0.88 0.84 4 8 0.76 0.91
0.87 0.83 Model 3 0.90 0.86 6 5 0.85 0.86 0.83 0.88 Model 4 0.93 0.90 1 7 0.79
0.98 0.96 0.86

Table 2: Model Performance Comparison

###  5.2 Model Results and Comparison

We evaluated each model using a prediction threshold to maximize the accuracy
and calculated performance metrics based on that threshold. The performance of
the four models are shown in tab:performance. Specifically, PPV, the positive
predictive value is defined as the percentage of true positives among all
cases predicted as positive; NPV, the negative predictive value is defined as
the percentage of true negatives among all cases predicted as negative. The
baseline model had an AUC-ROC of 0.79 and while the specificity was 1.0, the
sensitivity was 0.59. There were 14 false negatives; of these patients with no
record of ICD codes or medications in EHR, 8 were patients with subjective
concern or mild cognitive impairment (MCI) and 6 were patients with dementia.
The regular-expression based logistic regression had a substantial improvement
in performance over the baseline model with an AUC-ROC of 0.88. The percentage
of patients with dementia-related concepts shown in apd:app1; terms related to
memory and dementia-related medications had the highest coefficients in the
regression model. The sensitivity of detection improved to 0.76 but the
specificity was 0.91. The TF-IDF model demonstrated higher performance than
the regular expression-based model (AUC-ROC=0.90). The 20 words with the
highest correlation coefficients using TF-IDF vectorization are shown in
table:tdf in the Appendix B. The deep learning model outperformed all the
models (AUC-ROC=0.93). The patients misclassified in the models were
different, demonstrating that each model had its own advantages.

##  6 Conclusion and Future Work

We applied NLP algorithms to identify patients with cognitive concerns in EHR
and compared model performance. While the deep learning model’s performance
was the best, it was only marginally better than the term based NLP models. We
posit that deeper representations will be required for more complex tasks
requiring syntactical and contextual information such as classifying the stage
of cognitive impairment: MCI, mild, moderate or severe dementia. Our gold
standard set had a relatively smaller proportion of patients with subjective
concerns or mild cognitive impairment (28.6 % with cognitive concern), and the
overall sample size was small. To address these issues, we plan to implement
an active learning loop, starting from querying additional at-risk patients
over age 65 and without a dementia related ICD code or medication, and apply
the fine-tuned model to derive the probability of having cognitive concerns
for these patients. For the edge cases, the notes will be manually reviewed
and labeled. To improve the efficiency of this review process, we designed an
annotation tool that highlights the sections with regular expression matches
or higher attention weights (UI design in Appendix E). The new gold-standard
data will serve as the basis for the next iteration of the active learning
loop to further improve model performance and potentially detect patients with
an earlier stage of cognitive decline.

## References

  * Alzheimer’s Association [2019] Alzheimer’s Association.  2019 Alzheimer’s disease facts and figures.  _Alzheimer’s & Dementia_, 15(3):321–387, March 2019.  ISSN 15525260.  10.1016/j.jalz.2019.01.010.  URL http://doi.wiley.com/10.1016/j.jalz.2019.01.010.
  * Amjad et al. [2018] Halima Amjad, David L. Roth, Orla C. Sheehan, Constantine G. Lyketsos, Jennifer L. Wolff, and Quincy M. Samus.  Underdiagnosis of Dementia: an Observational Study of Patterns in Diagnosis and Awareness in US Older Adults.  _Journal of General Internal Medicine_ , 33(7):1131–1138, 2018.  ISSN 1525-1497.  10.1007/s11606-018-4377-y.
  * Amra et al. [2017] Sakusic Amra, John C. O’Horo, Tarun D. Singh, Gregory A. Wilson, Rahul Kashyap, Ronald Petersen, Rosebud O. Roberts, John D. Fryer, Alejandro A. Rabinstein, and Ognjen Gajic.  Derivation and validation of the automated search algorithms to identify cognitive impairment and dementia in electronic health records.  _Journal of Critical Care_ , 37:202–205, 2017.  ISSN 1557-8615.  10.1016/j.jcrc.2016.09.026.
  * Beltagy et al. [2020] Iz Beltagy, Matthew E Peters, and Arman Cohan.  Longformer: The long-document transformer.  _arXiv preprint arXiv:2004.05150_ , 2020.
  * Borson et al. [2013] Soo Borson, Lori Frank, Peter J. Bayley, Malaz Boustani, Marge Dean, Pei-Jung Lin, J. Riley McCarten, John C. Morris, David P. Salmon, Frederick A. Schmitt, Richard G. Stefanacci, Marta S. Mendiondo, Susan Peschin, Eric J. Hall, Howard Fillit, and J. Wesson Ashford.  Improving dementia care: the role of screening and detection of cognitive impairment.  _Alzheimer’s & Dementia: The Journal of the Alzheimer’s Association_, 9(2):151–159, March 2013.  ISSN 1552-5279.  10.1016/j.jalz.2012.08.008.
  * Devlin et al. [2018] Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova.  Bert: Pre-training of deep bidirectional transformers for language understanding.  _arXiv preprint arXiv:1810.04805_ , 2018.
  * Friedman et al. [2010] Jerome Friedman, Trevor Hastie, and Robert Tibshirani.  Regularization paths for generalized linear models via coordinate descent.  _Journal of Statistical Software_ , 33(1):1–22, 2010.  URL http://www.jstatsoft.org/v33/i01/.
  * Gilmore-Bykovskyi et al. [2018] Andrea L. Gilmore-Bykovskyi, Laura M. Block, Lily Walljasper, Nikki Hill, Carey Gleason, and Manish N. Shah.  Unstructured clinical documentation reflecting cognitive and behavioral dysfunction: toward an EHR-based phenotype for cognitive impairment.  _Journal of the American Medical Informatics Association: JAMIA_ , 25(9):1206–1212, 2018.  ISSN 1527-974X.  10.1093/jamia/ocy070.
  * Kingma and Ba [2014] Diederik P Kingma and Jimmy Ba.  Adam: A method for stochastic optimization.  _arXiv preprint arXiv:1412.6980_ , 2014.
  * Mikolov et al. [2013] Tomas Mikolov, Ilya Sutskever, Kai Chen, Greg S Corrado, and Jeff Dean.  Distributed representations of words and phrases and their compositionality.  In _Advances in neural information processing systems_ , pages 3111–3119, 2013.
  * Pennington et al. [2014] Jeffrey Pennington, Richard Socher, and Christopher D Manning.  Glove: Global vectors for word representation.  In _Proceedings of the 2014 conference on empirical methods in natural language processing (EMNLP)_ , pages 1532–1543, 2014.
  * Peters et al. [2018] Matthew E Peters, Mark Neumann, Mohit Iyyer, Matt Gardner, Christopher Clark, Kenton Lee, and Luke Zettlemoyer.  Deep contextualized word representations.  _arXiv preprint arXiv:1802.05365_ , 2018.
  * Rajapakse [2020] Thilina Rajapakse.  Simple transformers, 2020.  URL https://simpletransformers.ai/.
  * Reuben et al. [2017] David B. Reuben, Andrew S. Hackbarth, Neil S. Wenger, Zaldy S. Tan, and Lee A. Jennings.  An Automated Approach to Identifying Patients with Dementia Using Electronic Medical Records.  _Journal of the American Geriatrics Society_ , 65(3):658–659, 2017.  ISSN 1532-5415.  10.1111/jgs.14744.
  * Robinson et al. [2015] Louise Robinson, Eugene Tang, and John-Paul Taylor.  Dementia: timely diagnosis and early intervention.  _BMJ (Clinical research ed.)_ , 350:h3029, June 2015.  ISSN 1756-1833.  10.1136/bmj.h3029.
  * Sheu [2019] Yi-han Sheu.  _What Can AI Do in Precision Psychiatry? A Study in Electronic Health Records_.  PhD thesis, Harvard University, 2019.
  * Vaswani et al. [2017] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin.  Attention is all you need.  In _Advances in neural information processing systems_ , pages 5998–6008, 2017.
  * Wolf et al. [2019] Thomas Wolf, Lysandre Debut, Victor Sanh, Julien Chaumond, Clement Delangue, Anthony Moi, Pierric Cistac, Tim Rault, Rémi Louf, Morgan Funtowicz, Joe Davison, Sam Shleifer, Patrick von Platen, Clara Ma, Yacine Jernite, Julien Plu, Canwen Xu, Teven Le Scao, Sylvain Gugger, Mariama Drame, Quentin Lhoest, and Alexander M. Rush.  Huggingface’s transformers: State-of-the-art natural language processing.  _ArXiv_ , abs/1910.03771, 2019.

##  Appendix A Clinical Note Data Preprocessing Steps

In order to reduce the input unstructured data dimensionality and work with a
smaller vocabulary, we adopt a series of preprocessing steps to trim the notes
to reduce noise for all three proposed models. Those steps include:

  1. 1.

Removed all empty lines and multiple white spaces.

  2. 2.

Removed the fixed header section which only contains non-diagnostic info.

  3. 3.

Remove all note section content that was verified to be unimportant by experts
(either not relevant to the cognitive concern detection or contained the same
info already stored in structured data format outside the note space).

  4. 4.

Utilized SpaCy’s default name entity recognition package to detect and remove
certain non-relevant name entities includes date, time, person, quantity info.

  5. 5.

Removed all special characters and all other numbers after SpaCy entity
removal.

  6. 6.

Normalized all rest of the text to lower case.

  7. 7.

For model 4 only, we further used the tokenizer provided by the pre-trained
Longformer [4] model as tokenization in the model preprocessing steps, since
the Longformer tokenizer, like other attention-based model, has a its
particular way of handling out-of-vocabulary words.

##  Appendix B TF-IDF Feature Correlation Rank

tab:tfidf  Rank Terms CorrCoef 1 dementia 0.4364 2 memory 0.3587 3 daughter
0.2959 4 cognitive 0.2955 5 alzheimer 0.2940 6 accompanied 0.2890 7 behavioral
0.2809 8 unable 0.2756 9 confused 0.2754 10 donepezil 0.2738 11 mental 0.2686
12 aricept 0.2664 13 care 0.2580 14 impairment 0.2529 15 nursing 0.2402 16
assistance 0.2365 17 nurse 0.2306 18 living 0.2294 19 rn 0.2285 20 dnr 0.2271

Table 3: TF-IDF Vector Features Correlation

##  Appendix C Dementia Related Concepts

fig:regex

Figure 1: Dementia Related Concepts

##  Appendix D Longformer with Additional Sliding Windows

fig:longformer

Figure 2: Longformer Model with Additional Sliding Window Strategy

##  Appendix E Active Learning Annotation User Interface

fig:LabelingUI

Figure 3: Active Learning Annotation User Interface