# Path types and identity types in dependent type theory

There's been some debate at the nLab recently over the names of "identity type" and "path type" in certain dependent type theories.

One user wrote that

Many cubical type theorists make the distinction between identity types like Martin-Löf’s identity types, Swan’s identity types, and the higher observational type theory identity types, where the rules for the identity types all imply the definitional J rule as a theorem (and they call all 3 types ’identity types’), vs the cubical path types where the rules only imply the J rule up to a path, and additional regularity rules are needed to make the J rule definitionally valid.

but Mike Shulman says that

The identity types of higher observational type theory also do not satisfy definitional computation for J.

and a user named Nathan said that

Cubical type theorists make the distinction between path types and identity types because path types are literally functions out of an interval, just like how paths in Euclidean space are functions out of the unit interval, not because of the definitional/propositional J distinction. Otherwise, why are the types in XTT called “path types” instead of “identity types”? They satisfy definitional J by coercion and regularity.

Mike Shulman also wrote the two comments earlier in the discussion:

I would actually prefer that the phrase “identity type” be usable for whatever notion is appropriate for the particular type theory. This includes the Martin-Lof identity type (a.k.a. “jdentity type”), the path type of cubical type theroies, and the identity type of higher observational type theory, all of which satisfy different formal rules but are still “types of identifications”.

Yes, I’m aware that cubical type theorists tend to use “identity type” to mean the Martin-Lof one. (Although in cubical type theory there is also a “Swan identity type” that’s different from both path types and ML identity types.) I’m saying I would rather advocate a different usage. Some cubical type theorists have taken to calling the ML identity type the “jdentity type”, since its defining feature is the J rule.

In dependent type theory (such as homotopy type theory) both "path type" and "identity type" generally refer to type families whose categorical semantics in $$(\infty,1)$$-categories are path space objects. However, in most definitions, the type family is called "identity type"; this includes Per Martin-Löf's definition, Andrew Swan's definition, and Mike Shulman's definition in higher observational type theory. The sole exception to this seems to be in the various flavors of cubical type theory, where the corresponding type is called "path type". However, the induction principle for Martin-Löf's identity types is called "path induction", which along with the categorical semantics as path space objects indicates that "path type" may also be an appropriate name for the various other identity types.

Why are path types called path types in cubical type theory? And why aren't path types and identity types used interchangeably as synonyms elsewhere if all the types behave like path space objects?