Hedberg's Theorem

Definition

Hedberg’s Theorem states that any type $A$ with decidable equality is a hSet. $((x,y:A)\to (x=y)+\neg (x=y))\to \mathsf{isSet}(A)$

Significance

This result is crucial in HoTT because it proves that types with decidable equality cannot have non-trivial higher homotopical structure (higher paths). The proof works by constructing a function that maps any path $p:x=y$ to a canonical path determined by the decision procedure, thereby showing all parallel paths are equal.

References

• Hedberg, M. (1998). “A coherence theorem for Martin-Löf’s type theory”. Journal of Functional Programming.