Identity type (homotopy type theory)

NOTE: This page should be specific to identity types in homotopy type theory, and a separate node should exist for inductively-defined identity types.

In homotopy type theory, "equality" between two elements $\mathrm{Type}xyA$ is defined by a type $x{\equiv }_{A}y$ called the identity type — the type of identifications of the two elements.[cite:@rijke2022introduction] Identity types are proof-relevant and may have any number of inhabitants, each adorned with rich internal structure.

One of the most important differences between path types and inductively-defined identity types is that the J rule on paths only holds up to another path, but for inductively-defined identity types, J holds up to judgemental equality.[cite:@thenlabcubical]

Notation

Most authors denote the identity type as $x{=}_{A}y$ but since the ASCII equals sign is a reserved symbol of Agda, users commonly choose to use ⟨≡⟩ ($\equiv$), which authors typically reserve for definitional equality.[cite:@hottbook@rijke2025introduction@1lab] The Agda UniMath project uses ⟨＝⟩.[cite:@rijkeagdaunimath]