nLab Hedberg's theorem

Idea

Hedberg’s theorem in dependent type theory says that given a type $A$ with untruncated decidable equality, then $A$ it is an h-set. This was first proven in (Hedberg)

Theorem

Theorem

(Hedberg's theorem)

Suppose that $A$ is a type which has untruncated decidable equality. In other words, the projection

$$\array{Paths_A + (0\to A\times A)^{(Paths_A\to A\times A)}\\ \downarrow\\ A\times A}$$

(where $Paths_A$ is the path type of $A$, “+” forms the sum type, and on the right we have the $A \times A$-dependent function type into the empty type), has a section.

Then $A$ is a h-set.

Proof

Let $d$ be the given section. Thus, for any $x,y\colon A$, $d(x,y)$ is either a path from $x$ to $y$ or a function from $Paths(x,y)$ to the empty type (implying that $Paths(x,y)$ is also empty).

It suffices to exhibit an operation connecting any endo-path $p \in Paths(x,x)$ to the identity path $1_x$. Given such a path, define $q = d(x,x)$. If $d(x,x)$ lies in the second case, then $Paths(x,x)$ is empty, a contradiction since we know it contains $1_x$; hence we may assume $q\in Paths(x,x)$ as well.

Let $r$ be the image of $(1_x,p) \in Paths_{A\times A}((x,x),(x,x))$ under the section $d$. This is a path in the total space $Paths_A$ lying over the path $(1_x,p)$ in $A\times A$. Equivalently, it is a path in the fiber over $x$ from $(1_x,p)_*(d(x,x))$ to $d(x,x)$, where $(1_x,p)_*$ denotes transport in the fibration $Paths_A \to A\times A$ along the path $(1_x,p)$. However, we have defined $d(x,x) = q$, and transport in a path-space is just composition, so $r$ may be regarded as a path from $q p$ to $q$. Canceling $q$, we obtain a path from $p$ to $1_x$.

 See also

• h-set
• decidable equality

References

• Michael Hedberg, A coherence theorem for Martin-Löf’s type theory, J. Functional Programming, (1998)

• Nicolai Kraus, A direct proof of Hedberg’s theorem, blog post

• Nicolai Kraus, Martin Escardo, Thierry Coquand , Thorsten Altenkirch, Generalizations of Hedberg’s theorem, in M. Hasegawa (Ed.): TLCA 2013, LNCS 7941, pp. 173-188. Springer, Heidelberg 2013. (pdf)

• Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Project, Institute for Advanced Study, 2013. (web, pdf)