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?
Best Answer
Prior to about a decade ago, no one used "path" terminology for identity types. The identification of the semantics of identity types with path objects dates to Awodey and Warren's Homotopy theoretic models of identity types and Voevodsky's simplicial model of univalent foundations. After this, some people working in homotopy type theory started calling Martin-Lof identity types (which were the only ones being used at that time) "path types" and their elements "paths" to emphasize the homotopical intuition. This perspective was ascendant when the HoTT Book was written, and is the origin of the phrase "path induction" for identity elimination.
A little while after that, some of us started to back off from this terminology, partly because of rising interest in topological/cohesive models and versions of type theory, where in addition to the "homotopical" notion of "path" encoded by the identity types, there is a separate unrelated "topological" notion of "path" represented by actual functions out of an actual interval. (In fact, of course, topological paths also exist in Book HoTT, as soon as you define real numbers and topological spaces!) To reserve "path" for topological notions, we started to return to the terminology "identity type" and call their elements "identifications".
Separately and unrelatedly, cubical type theory arrived on the scene with two or even three notions of "identity type", which therefore needed different names to distinguish them. I was not one of the inventors of cubical type theories, so I can't say with certainty why its "path types" are called thusly, but I expect Nathan has it right. Unlike Martin-Lof identity types, cubical path types really are "paths" in the sense of "function out of an interval", although the interval is a primitive object (not even a type) rather than a topological set of real numbers. So inside cubical type theory, it makes some sense to reserve "path type" for those and "identity type" for the others.