  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 Catt, 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 Catt$_{sa}$, 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.
