I would object to the characterization of definitional identity as identity of sense. Sense is often glossed as mode of givenness; or one might say that the sense of an expression determines a route to its reference. Now take terms such as 7+5 and 9+3. These are definitionally identical, but they present the number twelve in different ways; qua senses each determines a different route to ssssssssssss(0). Hence they are not the same senses. Identity of sense is, to my mind, a stricter relation than definitional identity.
Very often, also in this thread, the notions of judgemental identity and definitional identity seem to be treated as one and the same thing. But by judgemental identity we should mean a certain form of identity assertion that is different from the assertion that an identity proposition/type is true/inhabited; and by definitional identity we should mean one among several relations on terms that may properly be called a relation of identity.
Here is an argument for the need of a form of identity assertion other than p : Id(A,a,b). The proposition Id(A,a,b) is formed by applying the function Id to the type of individuals (set in Martin-Löf's terminology) A, and the elements a,b : A. The notion of a function, however, presupposes a notion of identity: f is a function only if, when applied to identical arguments a, b, we get identical results f(a), f(b). On pain of circularity, the notion of identity appealed to here cannot be propositional identity.
A notion of identity is also implicit in the notion of domain presupposed by the notion of a function: f is a function from the domain A to the domain B. To have the right to speak of A as a domain we need to know what it is for elements of A to be identical, we need to know a criterion of identity for A.
In type theory the alternative form of identity assertion, used for instance in the explanation of what a function is, is the identity judgement a = b : A. There is nothing in the argument just given that forces the relation picked out by this form of identity assertion to be definitional identity; but there may be other arguments why such an interpretation is preferable.