There are two usual ways to describe equality in a dependent typing system, one that uses an external notion of computation like β-reduction, and one that introduces a typed judgement of β-equality directly in the typing system. After being open for some time, the equivalence between both approaches has been solved by Adams for a rather large class of pure type systems (PTSs) called functional. Unfortunately, the constraint of functionality prevents the extension to systems with sub-typing, and especially to systems like the Extended Calculus of Constructions on which a system commonly used like Coq is rooted. In this paper, we shall 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, this result should eventually bring closer the theory behind the proof assistant Coq to its implementation.
slides
Read Me
Coq files
tar file: Tested with the trunk version of Coq. Almost compatible with v8.2 with a minor syntactic changes when using destruct.
Please modify the Makefile to point out where coqc is located.