Identity types: What makes Intuitionistic Type Theory *intuitionistic*?

Question

In the opening passage of Martin-Löf's (1975) he famously says that

"the theory of types with which we shall be concerned is intended to be a full scale system for formalizing intuitionistic mathematics".

Although we are dealing with type theory and not logic, the proposition-as-types paradigm teaches us how the introduction and elimination rules for, say, product types or function types, can be justified by the BHK informal semantics - in this case, conjuncion and implication, respectively.

However, what about the identity type - the sugar of Martin-Löf Type Theory (MTT)?

Specifically, I am concerned about the intuitionistic justification of the elimination rule of the identity type in the intensional version of MTT. The point is that, as far as I am concern, the BHK interpretation is limited to explain the meaning of conjunction, disjunction, implication, contradiction, existential and universal quantifiers as logical constants, but it has absolutely nothing to say about identity. (I wonder if Brouwer et al have held any position in respect to identity?)

Question:

Can we intuitionistically justify the elimination rule of the identity type?

My initial guess is that the rule can be substantiated via the meaning explanations, but I am not sure in which extent it characterizes the intuitionistic position: it is undoubtedly a constructive position though, more like in Bishop's sense.

Answer 1

As far as I can tell Martin-Löf's analysis of identity and his formulation of the identity types is the intuitionistic explanation of identity. In terms of BHK it would be an algorithmic version of Leibniz's rule:

A proof of $a = b$ is a method which, for any predicate $P$, produces from any proof of $P(a)$ a proof of $P(b)$.

We can then justify $a = a$ by the method $\lambda \zeta . \zeta$. However this sort of explanation is quite a bit more complicated than the rest of the BHK interpretation because the method takes a predicate $P$ as input. It is no surprise that it was not discovered at the same time as the rest of BHK.

Many people before Martin-Löf simply side-stepped the question of identity by simplifying things. One way of doing this is to consider a formal system with a limited supply of basic types whose identity is decidable. This happens, for instance, in Heyting arithmetic.

Bishop's way of dealing with identity was to say that a set is given by something like a collection of elements and an equivalence relation on them. They type-theoretic analogue of this are the setoids. This kind of treatment of identity is not entirely satisfactory. For instance, you can ask how we can tell whether two elements are actually equal.

There are Mathoverflowers who are more knowledgable about the history of intuitionisism. Let's hope they can shed some light.

Answer 2

You are right to note that Martin-Löf's treatment of identity as a type is an extension of the BHK-interpretation as originally presented by H(eyting) and K(olmogorov/reisel).

Your guess is also right that Id-elimination can be justified on the basis of Martin-Löf's meaning explanations for his type theory. First it must be clarified what it means to justify this rule.

$$\begin{array}{l} p:\mathrm{Id}(A,a,b) \\ z:A\vdash c:C[z,z,\mathrm{refl}(A,z)]\\ \hline J(p,z.c):C[a,b,p] \end{array}$$

In order to justify the rule one must make the conclusion evident on the assumption that one knows the premisses. To make the conclusion evident requires, according to the meaning-explanations, to make it evident that $J(p, z.c)$ evaluates to a canonical object in $C[a,b,p]$.

Assuming that we know $p:\mathrm{Id}(A,a,b)$, we know, by the explanation of the form of judgement $a:A$ that $p$ evaluates to a canonical element of $\mathrm{Id}(A,a,b)$. We stipulate, in general, that a canonical element of type $\mathrm{Id}(A,a,b)$ has the form

$$\mathrm{refl}(A', a')$$

where

$$A=A':type\\ a = a' : A \\ b = a' : A $$

Hence we know

$$p=\mathrm{refl}(A', a')=\mathrm{refl}(A,a):\mathrm{Id}(A,a,b)$$

Therefore

$$J(p, z.c)=J(\mathrm{refl}(A,a), z.c)=c[a]:C[a,a,\mathrm{refl}(A,a)]$$

where the final equality follows from the (definitional) rule of Id-equality.

By the (judgemental) equalities already stated we have

$$C[a,a,\mathrm{refl}(A,a)]=C[a,b,p]:type$$

By the premiss $z:A\vdash c:C[z,z,\mathrm{refl}(A,z)]$ and the meaning explanation for hypothetical judgements, we therefore know that $c[a]$ evaluates to a canonical object in $C[a,b,p]$.

It follows then from the meaning explanation for the form of judgement $a=b:A$ that $J(p, z.c)$ also evaluates to such a canonical object.

For more details perhaps I can refer to a paper of mine, forthcoming (at the time of writing) in Topoi, The justification of identity elimination in Martin-Löf's type theory.