The identity type has elements that are witnesses to the βsamenessβ of elements.
The identity type $=_A : A \to A \to \mathcal{U}$ can be defined as the inductive type? with the following constructor:
Identity types have the following formation rule
Univalent Foundations Project, Homotopy Type Theory β Univalent Foundations of Mathematics (2013)
Mike Shulman, Towards a Third-Generation HOTT Part 1 (slides, video)