Path induction

In homotopy type theory, path induction refers to the induction principle of identity types $x{\equiv }_{A}y$. Informally, path induction declares that, to prove that some proposition holds for $x{\equiv }_{A}y$, it suffices to consider the reflexivity case $\mathrm{refl}:x{\equiv }_{A}x$.

Path induction is one of the most subtle aspects of HoTT, and is key to understanding the differences between HoTT's paths and inductively-defined identity types.Inductively-defined identity types are the usual equality types used in Idris and (non-cubical) Agda: a simple data type _≡_ : (x y : A) → Type with a single constructor refl : x ≡ x. "A single constructor" is the most important detail here. Inductively-defined identity types are trivial singletons. One inhabitant. Zero complex structure. This is completely opposite to path types, which are not inductively-defined (they are taken as primitive) and possess rich structure relating the identified types. Two arbitrary identifications $p,q:x\equiv y$ are not necessarily the same in HoTT (i.e. UIP does not hold). [cite:@hottbook]

Statement

Given a family $$D:\prod _{a,a^{\prime }:A}a\equiv a^{\prime }\to 𝒰$$ and a dependent function $$d:\prod _{a:A}Daa\mathrm{refl},$$ path induction gives us a dependent function $$f:\prod _{(a,a^{\prime }:A)}\prod _{(p:a\equiv a^{\prime })}Da{a}^{\prime }p$$ defined by the equation $$faa\mathrm{refl}≔da.$$

Path induction has an equivalent formation that is occasionally convenient, called based path induction.[cite:@hottbook] This is the variant used in Agda's cubical library:

Fix an element $a:A$, and suppose a family $$C:\prod _{x:A}(a{\equiv }_{A}x)\to 𝒰,$$ and an element $$c:Ca{\mathrm{refl}}_a.$$ We then obtain a function $$f:\prod _{(x:a)}\prod _{(p:a\equiv x)}Cxp$$ defined by the equation $$fa{\mathrm{refl}}_a:=c.$$

Traditionally, (based) path induction is packaged up as a single function and called $J$.[cite:@hottbook]

Corollaries

Many important properties of paths follow from path induction, including invertibility and concatenation:Or, the language of relations, symmetry and transitivity.

  private variable
    ℓ ℓ' ℓ'' : Level

  module _ {A : Type ℓ}
           (C : (a a' : A) → a ≡ a' → Type ℓ')
           (c : ∀ a → C a a refl)
           where

    ≡-ind : ∀ a a' p → C a a' p
    ≡-ind a a' p = J (C a) (c a) p
    
    ≡-ind-refl : ∀ a → ≡-ind a a refl ≡ c a
    ≡-ind-refl a = JRefl (λ y z → y) (c a)

  inv : {A : Type ℓ} {x y : A} → x ≡ y → y ≡ x
  inv = ≡-ind D d _ _ where

    D : ∀ x y → x ≡ y → Type _
    D x y _ = y ≡ x

    d : ∀ x → D x x refl
    d x = refl

  -- ≡-concatˡ refl p ≡ p follows from ≡-ind-refl.
  ≡-concatˡ : {x y z : A} → x ≡ y → y ≡ z → x ≡ z
  ≡-concatˡ {A = A} = λ p q → ≡-ind D d _ _ p _ q where

    D : (x y : A) → x ≡ y → Type _
    D x y _ = ∀ z → y ≡ z → x ≡ z

    d : ∀ x → D x x refl
    -- ∀ x z → x ≡ z → x ≡ z
    d x z p = p

  -- ≡-concatʳ p refl ≡ p follows from ≡-ind-refl.
  ≡-concatʳ : {x y z : A} → x ≡ y → y ≡ z → x ≡ z
  ≡-concatʳ {A = A} = λ p q → ≡-ind D d _ _ q _ p where

    D : (y z : A) → y ≡ z → Type _
    D y z _ = ∀ x → x ≡ y → x ≡ z

    d : ∀ y → D y y refl
    -- ∀ y x → x ≡ y → x ≡ y
    d x z p = p

References

• [cite:@hottbook]