As we mentioned above, identity on natural numbers can be defined by primitive recursion. Identity relations on other types can also be defined in the basic version of intuitionistic type theory presented in section 2.