Path Type (HoTT)

Definition

The path type (or identity type) represents the concept of equality between two terms of the same type. For a type $A$ and terms $a,b:A$, the path type is denoted $a{=}_{A}b$ (or ${\mathsf{Id}}_A(a,b)$). In Homotopy Type Theory, elements of $a{=}_{A}b$ are interpreted as paths from $a$ to $b$ in the space $A$, rather than mere witnesses of a property.

Rules (Martin-Löf)

We define the type inductively.

Formation

Given $A:\mathcal{U}$ and $a,b:A$, we have a type $(a{=}_{A}b):\mathcal{U}$.

Introduction

For every $a:A$, there is a canonical element representing the constant path: ${\mathsf{refl}}_a:a{=}_{A}a$

Elimination (Path Induction)

To prove a indexed family $P$ for all paths, it suffices to prove it for reflexivity, provided that one endpoint is free ¹. Let $P:{\prod }_{x,y:A}(x{=}_{A}y)\to \mathcal{U}$. Given a proof for reflexivity: $d:{\prod }_{x:A}P(x,x,{\mathsf{refl}}_x)$ We construct a term: $J(P,d):{\prod }_{x,y:A}{\prod }_{p:x=y}P(x,y,p)$

Computation

The eliminator applied to the canonical constructor reduces to the given proof term: $J(P,d,x,x,{\mathsf{refl}}_x)\equiv d(x)$

Cubical Type Theory

In Cubical Type Theory, the path type is not defined inductively but as a map from an abstract interval type $\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$. Path induction is derived from transport and the structure of the interval, rather than being axiomatic. Functional extensionality and univalence become provable theorems (or definitions) rather than axioms.

Properties

1. Symmetry: $p^{-1}:y=x$ for $p:x=y$.
2. Transitivity: $p\cdot q:x=z$ for $p:x=y,q:y=z$.
3. Transport: Given $P:A\to \mathcal{U}$ and $p:x=y$, we have ${\mathsf{transport}}^P(p):P(x)\to P(y)$.
4. Groupoid Structure: Types form $\infty$-groupoids where paths correspond to morphisms.

Agda

In Agda --cubical, the path type is a primitive.

open import Agda.Primitive
 
-- The path type is distinct from the inductive _≡_
_≡_ : {ℓ : 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

Footnotes

Footnotes

1. This is needed in HoTT because we are constructing a singleton, which needs to be a contraction for the construction to give a single path output. Without that we can’t say that the path can be reached from refl. Consider $S^1$. ↩