The computational content of equality in Martin-Löf type theory
If you ask a type theorist what "axioms" their system assumes, you may get a look of indignation. Type theorists take pride in assuming no axioms. Instead, a type theory has grammatical rules which allow the user to define types and terms. An "axiom" in the context of type theory refers to an assumption that a certain type is inhabited, even when it is impossible to construct a term of the given type purely by following the grammatical rules. The distinction may sound like mere semantics; but a type theory is a programming language, and the constructions of the grammar have computational content even when their logical meaning is ignored. One need not appeal to any kind of logical principles in justifying the terms; one can justify them only in terms of programming. Equality in (intensional) Martin-Löf type theory is strangely behaved. In MLTT, proofs of equality are mathematical objects in their own right that can be referred to within the theory. In particular,...