  We use type-theoretic techniques to present an algebraic theory of
$\infty$-categories with strict units. Starting with a known type-theoretic
presentation of fully weak $\infty$-categories, in which terms denote valid
operations, we extend the theory with a non-trivial definitional equality. This
forces some operations to coincide strictly in any model, yielding the strict
unit behaviour.
  We make a detailed investigation of the meta-theoretic properties of this
theory. We give a reduction relation that generates definitional equality, and
prove that it is confluent and terminating, thus yielding the first decision
procedure for equality in a strictly-unital setting. Moreover, we show that our
definitional equality relation identifies all terms in a disc context,
providing a point comparison with a previously proposed definition of strictly
unital $\infty$-category. We also prove a conservativity result, showing that
every operation of the strictly unital theory indeed arises from a valid
operation in the fully weak theory. From this, we infer that strict unitality
is a property of an $\infty$-category rather than additional structure.
