Equality Is Typable in Semi-full Pure Type Systems

There are two usual ways to describe equality in a dependent typing system, one that uses an external notion of computation like beta-reduction, and one that introduces a typed judgement of beta-equality directly in the typing system. After being an open problem for some time, the general equivalence between both approaches has been solved by Adams for a class of pure type systems (PTSs) called functional. In this paper, we relax the functionality constraint and prove the equivalence for all semi-full PTSs by combining the ideas of Adams with a study of the general shape of types in PTSs. As one application, an extension of this result to systems with sub-typing would be a first step toward bringing closer the theory behind a proof assistant such as Coq to its implementation.