  We present a general and user-extensible equality checking algorithm that is
applicable to a large class of type theories. The algorithm has a type-directed
phase for applying extensionality rules and a normalization phase based on
computation rules, where both kinds of rules are defined using the
type-theoretic concept of object-invertible rules. We also give sufficient
syntactic criteria for recognizing such rules, as well as a simple
pattern-matching algorithm for applying them. A third component of the
algorithm is a suitable notion of principal arguments, which determines a
notion of normal form. By varying these, we obtain known notions, such as weak
head-normal and strong normal forms. We prove that our algorithm is sound. We
implemented it in the Andromeda~2 proof assistant, which supports
user-definable type theories. The user need only provide the equality rules
they wish to use, which the algorithm automatically classifies as computation
or extensionality rules, and select appropriate principal arguments.
