Identity Type

Idea

In type theory, an identity type is a the type of proofs that two terms are equal.

Definition

The identity type (or path type) represents the concept of equality between two terms of the same type. For a type $A$ and terms $a,b:A$, the type is denoted $a{=}_{A}b$ or ${\mathsf{Id}}_A(a,b)$. Unlike definitional equality, which is a metatheoretic judgment, the identity type is a type within the theory whose terms represent witnesses of equality.

Perspective

In HoTT, terms of $a{=}_{A}b$ are interpreted as paths from $a$ to $b$ in the space $A$. This view generalizes the notion of a witness to a path in an $\infty$-groupoid, where multiple distinct paths may exist between the same points.

Formation

$\frac{\Gamma ⊢A\text{ type}\Gamma ⊢a:A\Gamma ⊢b:A}{\Gamma ⊢a{=}_{A}b\text{ type}}$

Given a type and two terms of that type, we can form the type of identifications between them.

Introduction

$\frac{\Gamma ⊢a:A}{\Gamma ⊢{\mathsf{refl}}_a:a{=}_{A}a}$

For any term $a$, there is a canonical witness of its equality with itself, representing the constant path.

Elimination (Path Induction)

$\frac{\Gamma ,x:A,y:A,p:x{=}_{A}y⊢P\text{ type}\Gamma ,z:A⊢d:P[z,z,{\mathsf{refl}}_z]}{\Gamma ,x:A,y:A,p:x{=}_{A}y⊢J(P,d,x,y,p):P}$

To prove a property $P$ for all paths, it suffices to provide a proof for the case where the path is reflexivity. This requires at least one endpoint to be free.

Computation

$\frac{\Gamma ,x:A,y:A,p:x{=}_{A}y⊢P\text{ type}\Gamma ,z:A⊢d:P[z,z,{\mathsf{refl}}_z]}{\Gamma ,z:A⊢J(P,d,z,z,{\mathsf{refl}}_z)\equiv d:P[z,z,{\mathsf{refl}}_z]}$

The eliminator applied to the reflexivity constructor reduces definitionally to the proof provided for the reflexive case.

Properties

• Symmetry: For $p:x=y$, there exists $p^{-1}:y=x$.
• Transitivity: For $p:x=y$ and $q:y=z$, there exists $p\cdot q:x=z$.
• Transport: Given $P:A\to \mathcal{U}$ and $p:x=y$, there is a map ${\mathsf{transport}}^P(p):P(x)\to P(y)$.
• hLevel: An identity type is not necessarily a mere proposition. Its complexity depends on the hLevel of $A$.

Cubical Type Theory

In Cubical Type Theory, the path type is not inductive but defined via a map from an abstract interval $\mathbb{I}$:

$x{=}_{A}y:\equiv {\prod }_{i:\mathbb{I}}A[i=0\mapsto x,i=1\mapsto y]$

Here, $\mathsf{refl}$ is the constant map $\lambda i.x$. This formulation provides computational content to the Univalence Principle and function extensionality.

References

• martin-lof1984-mltt
• hoffmann1997-dependent-types
• hott2013-book
• rijke2022-hott