However, Martin-Löf (1975) extended intuitionistic type theory with a uniform primitive identity type former \(\I\) for all types. The rules for \(\I\) express that the identity relation is inductively generated by the proof of reflexivity, a canonicial constant called \(\r\). (Note that \(\r\) was coded by the number 0 in the introductory presentation of proof-objects in 2.3. The elimination rule for the identity type is a generalization of identity elimination in predicate logic and introduces an elimination constant \(\J\). We here show the formulation due to Paulin-Mohring (1993) rather than the original formulation of Martin-Löf (1975). The inference rules are the following.