# Contents

## 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

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$.