The \(\I\)-type is often called the intensional identity type, since it does not satisfy the principle of function extensionality. Intuitionistic type theory with the intensional identity type is also often called intensional intuitionistic type theory to distinguish it from extensional intuitionistic type theory which will be presented in  section 7.1.