Identity Type

Idea

In type theory, the identity type $a{=}_{A}b$ is the type of proofs that two terms $a,b:A$ are equal. Unlike definitional equality, which is a judgement external to the theory, the identity type lives inside the theory: its terms are witnesses of equality, and the type may have rich structure.

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

Definition

For a type $A:\mathcal{U}$ and terms $a,b:A$, the identity type is denoted $a{=}_{A}b$ or ${\mathsf{Id}}_A(a,b)$. The subscript $A$ is often omitted when it is clear from context.

Rules

Formation

$\frac{\Gamma ⊢A:\mathcal{U}\Gamma ⊢a:A\Gamma ⊢b:A}{\Gamma ⊢a{=}_{A}b:\mathcal{U}}$

Introduction

The only constructor is reflexivity: every term is equal to itself. Note that other computation rules
$\frac{\Gamma ⊢a:A}{\Gamma ⊢{\mathsf{refl}}_a:a{=}_{A}a}$

Elimination (path induction)

To prove a property $P$ for all paths, it suffices to prove it for reflexivity, provided that one endpoint is free.¹ Given a motive $P:(x,y:A)\to (x{=}_{A}y)\to \mathcal{U}$ and a proof for the reflexive case:
$d:(x:A)\to P(x,x,{\mathsf{refl}}_x)$
the J eliminator constructs a term:
$J(P,d):(x,y:A)\to (p:x{=}_{A}y)\to P(x,y,p)$

In inference rule form:
$\frac{\Gamma ,x:A,y:A,p:x{=}_{A}y⊢P:\mathcal{U}\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}$

Computation

The eliminator reduces on reflexivity:
$J(P,d,x,x,{\mathsf{refl}}_x)\equiv d(x)$

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: $a{=}_{A}b$ is not necessarily a mere proposition; its complexity depends on the hLevel of $A$.
• Groupoid structure: types form $\infty$-groupoids where paths are morphisms, higher paths are 2-morphisms, and so on.

Cubical Type Theory

In Cubical Type Theory, the path type is not defined inductively. Instead, a path from $x$ to $y$ in $A$ is a function out of the abstract interval type $\mathbb{I}$ satisfying face constraints:

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

Reflexivity is the constant map ${\mathsf{refl}}_x:\equiv \lambda i.x$. Under this definition, path induction is derived from transport and the structure of $\mathbb{I}$ rather than being axiomatic, and function extensionality and univalence become provable.

Agda

In Agda --cubical, the path type is a primitive distinct from the inductive propositional equality _≡_.

open import Agda.Primitive
 
_≡_ : {ℓ : Level} {A : Set ℓ} → A → A → Set ℓ
x ≡ y = PathP (λ _ → A) x y
 
refl : {ℓ : Level} {A : Set ℓ} {x : A} → x ≡ x
refl {x = x} = λ i → x

Related Concepts

• J Eliminator
• Definitional Equality
• Transport
• Homotopy Level
• Singleton Type
• Univalence Principle

References

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

Footnotes

1. One endpoint must be free because the construction corresponds to showing the singleton type $(x:A)\times (a=x)$ is contractible. With both endpoints fixed, the path space is not generally contractible — consider loops on $S^1$. ↩