Hedberg: A coherence theorem for Martin-Löf type theory

MICHAEL HEDBERG: A coherence theorem for Martin-Löf’s type theory
J. Functional Programming 8 (4): 413–436, July 1998.

Abstract
In type theory a proposition is represented by a type, the type of its proofs. As a consequence, the equality relation on a certain type is represented by a binary family of types. Equality on a type may be conventional or inductive. Conventional equality means that one particular equivalence relation is singled out as the equality, while inductive equality – which we also call identity – is inductively defined as the ‘smallest reflexive relation’. It is sometimes convenient to know that the type representing a proposition is collapsed, in the sense that all its inhabitants are identical. Although uniqueness of identity proofs for an arbitrary type is not derivable inside type theory, there is a large class of types for which it may be proved.
Our main result is a proof that any type with decidable identity has unique identity proofs. This result is convenient for proving that the class of types with decidable identities is closed under indexed sum. Our proof of the main result is completely formalized within a kernel fragment of Martin-Löf’s type theory and mechanized using ALF. Proofs of auxiliary lemmas are explained in terms of the category theoretical properties of identity. These suggest two coherence theorems as the result of rephrasing the main result in a context of conventional equality, where the inductive equality has been replaced by, in the former, an initial category structure and, in the latter, a smallest reflexive relation.

Capsule Review
This paper offers new results about propositional equality in Martin-Löf ’s intensional type theory. The main result states that if equality on a type A is decidable, then any two proofs of equality between elements of A are equal themselves. This seemingly academic question is of immediate practical relevance for programming with dependent types. For example, if we model many-sorted stores as where is a type-valued function assigning types to locations, then to establish the expected properties of updating such stores we need to know that any two proofs of location equality are equal (example due to Thomas Schreiber). The main result guarantees this under the reasonable assumption that equality of locations is decidable.
A possible obstacle for readers that are not experts in Martin-Löf type theory is the fact that (following recent tradition) the paper uses intentional type theory in which propositional equality is witnessed by proof objects and in which (unlike in extensional type theory) type checking is decidable, but that in the context of extensional type theory (which is perhaps better known) the results in the paper are trivial.