nLab Hedberg's theorem



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



(Hedberg's theorem)

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

Paths A+(0A×A) (Paths AA×A) A×A\array{Paths_A + (0\to A\times A)^{(Paths_A\to A\times A)}\\ \downarrow\\ A\times A}

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

Then AA is a h-set.


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

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

Let rr be the image of (1 x,p)Paths A×A((x,x),(x,x))(1_x,p) \in Paths_{A\times A}((x,x),(x,x)) under the section dd. This is a path in the total space Paths APaths_A lying over the path (1 x,p)(1_x,p) in A×AA\times A. Equivalently, it is a path in the fiber over xx from (1 x,p) *(d(x,x))(1_x,p)_*(d(x,x)) to d(x,x)d(x,x), where (1 x,p) *(1_x,p)_* denotes transport in the fibration Paths AA×APaths_A \to A\times A along the path (1 x,p)(1_x,p). However, we have defined d(x,x)=qd(x,x) = q, and transport in a path-space is just composition, so rr may be regarded as a path from qpq p to qq. Canceling qq, we obtain a path from pp to 1 x1_x.

 See also


Created on December 8, 2022 at 19:51:19. See the history of this page for a list of all contributions to it.