Encode-decode method

In homotopy type theory, the encode-decode method is a technique used to characterise the path space of a given type. The process begins by defining a "coding" on a type, concretely giving the expected behaviour of the abstract identity type.

  code : ℕ → ℕ → Type
  code zero    zero    = Unit
  code zero    (suc n) = ⊥
  code (suc m) zero    = ⊥
  code (suc m) (suc n) = code m n

Then, this type is related to the path type, usually including an equivalence $\mathrm{code}xy\simeq (x\equiv y)$. The encode-decode technique can also be used to prove disequalities between different constructors.