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.