nLab identification

Idea

In dependent type theory, and particularly homotopy type theory, an identification is a word sometimes used for an inhabitant of an identity type. Alternatives to the term identification include identity, path, or equality, though those phrases are also used in different contexts.

Thus an identification $p:\mathrm{Id}(a, b)$ provides a “reason”, a “witness”, or a “proof” that $a$ and $b$ “are equal”, or more precisely a way in which to identify them. one can say that $a$ and $b$ are identified. The distinguishing feature of homotopy type theory is that in general, there may be more than one way to identify two things, i.e. more than one identification between two given elements.

See also

• function application to identities
• transport
• unique identification

References

• Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (arXiv:2212.11082)

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)