Any type A that has decidable equality is a set. Assuming H_A:\mathsf {hasDecEq(A)}, we must check that for all x,y:A and p,q:x=_Ay we have p=_{x=_Ay}q. Putting that aside for now, we first consider that when an individual identification type x=_Ay is decidable, we can “replace” any specific identification p:x=_Ay with the result of the decision procedure.
\begin {aligned}
&\mathsf {repl}_{x,y}:\mathsf {isDec}(x=_Ay)\to x=_Ay\to x=_Ay
\\
&\mathsf {repl}_{x,y}~(\mathsf {inl}~q)~p :\equiv q
\\
&\mathsf {repl}_{x,y}~(\mathsf {inr}~h)~p :\equiv \mathsf {abort}~(hp)
\end {aligned}
We can show that for each d:\mathsf {isDec}(x=_Ay), the function \mathsf {repl}_{x,y}~d is weakly constant without much difficulty by cases on d:
\begin {aligned}
&\mathsf {replIsWeaklyConstant}_{x,y}:
{\mathop {\mathchoice {\textstyle \prod }{\textstyle \prod }{\scriptstyle \prod }{\scriptscriptstyle \prod }
}_{(d:\mathsf {isDec}(x=_Ay))}}
\mathsf {isWeaklyConstant}~(\mathsf {repl}_{x,y}~d)
\\
&\mathsf {replIsWeaklyConstant}_{x,y}~(\mathsf {inl}~r)~p~q :\equiv \mathsf {refl}_{r}
\\
&\mathsf {replIsWeaklyConstant}_{x,y}~(\mathsf {inr}~h)~p~q :\equiv
\mathsf {abort}~(hp)
\end {aligned}
Unfortunately, we cannot seem to show that \mathsf {repl}_{x,y}~d is the identity function. Indeed, to define the case for d\equiv \mathsf {inl}~r we would need to show that any identification p:x=_Ay is equal to r, which is just as hard as our main goal. We can wriggle out of this tough spot using a trick we’ve seen before: we can “pad” \mathsf {repl}_{x,y} with a flipped instance of \mathsf {refl}_{x,x} on either the left-hand or the right-hand side. Then later on, the two will cancel out. Using our witness h_A:\mathsf {hasDecEq}(A), let us define a new function to “clean” an identification:
\begin {aligned}
&\mathsf {clean}^{h_A}_{x,y}:x=_Ay\to x=_Ay
\\
&\mathsf {clean}^{h_A}_{x,y}~p :\equiv
\overline {
\mathsf {repl}_{x,x}~(h_Axx)~\mathsf {refl}_x
}
\cdot
\mathsf {repl}_{x,y}~p
\end {aligned}
First we check that \mathsf {clean}_{x,y} is the identity function:
\begin {aligned}
&
\mathsf {cleanIsIdentity}_{h_A}:
{\mathop {\mathchoice {\textstyle \prod }{\textstyle \prod }{\scriptstyle \prod }{\scriptscriptstyle \prod }
}_{(x,y:A)}}
\mathsf {isIdentity}(\mathsf {clean}^{h_A}_{x,y})
\\
&
\mathsf {cleanIsIdentity}_{h_A}~x~y~p :\equiv
\bigl \{
?:
\mathsf {clean}^{h_A}_{x,y}~p =_{x=_Ay} p
\bigr \}
\end {aligned}
We proceed by identification elimination on (y,p) and unravel the definition of \mathsf {clean}:
\begin {aligned}
&
\mathsf {cleanIsIdentity}_{h_A}:
{\mathop {\mathchoice {\textstyle \prod }{\textstyle \prod }{\scriptstyle \prod }{\scriptscriptstyle \prod }
}_{(x,y:A)}}
\mathsf {isIdentity}(\mathsf {clean}^{h_A}_{x,y})
\\
&
\mathsf {cleanIsIdentity}_{h_Axx}~\mathsf {refl}_x :\equiv
\bigl \{
?:
\overline {
\mathsf {repl}_{x,x}~(h_Axx)~\mathsf {refl}_x
}
\cdot
\mathsf {repl}_{x,x}~(h_Axx)~\mathsf {refl}_x
=_{x=_Ax}
\mathsf {refl}_x
\bigr \}
\end {aligned}
But that is just the left unit law for flipping:
\begin {aligned}
&
\mathsf {cleanIsIdentity}_{h_A}:
{\mathop {\mathchoice {\textstyle \prod }{\textstyle \prod }{\scriptstyle \prod }{\scriptscriptstyle \prod }
}_{(x,y:A)}}
\mathsf {isIdentity}(\mathsf {clean}^{h_A}_{x,y})
\\
&
\mathsf {cleanIsIdentity}_{h_A}~x~x~\mathsf {refl}_x :\equiv
\mathsf {flipLeftUnit}(\mathsf {repl}_{x,x}~(h_Axx)~\mathsf {refl}_{x})
\end {aligned}
We still need to check that \mathsf {clean}^{h_A}_{x,y} is weakly constant; luckily, we can reuse our proof that \mathsf {repl}_{x,y} is weakly constant:
\begin {aligned}
&
\mathsf {cleanIsWeaklyConstant}^{h_A}_{x,y}
:
\mathsf {isWeaklyConstant}(\mathsf {clean}^{h_A}_{x,y})
\\
&
\mathsf {cleanIsWeaklyConstant}^{h_A}_{x,y}~p~q :\equiv
\\
&\quad
\bigl \{
?:
\overline {\mathsf {repl}_{x,x}~(h_Axx)~\mathsf {refl}_x}
\cdot
\mathsf {repl}_{x,y}~(h_Axy)~p
=_{x=_Ay}
\overline {\mathsf {repl}_{x,x}~(h_Axx)~\mathsf {refl}_x}
\cdot
\mathsf {repl}_{x,y}~(h_Axy)~q
\bigr \}
\end {aligned}
We already know that \mathsf {repl}_{x,y}~(h_Axy)~p=_{x=_Ay}\mathsf {repl}_{x,y}~(h_Axy)~q because we have shown that \mathsf {repl}_{x,y} is weakly constant. So we use the action on identifications:
\begin {aligned}
&
\mathsf {cleanIsWeaklyConstant}_{x,y}
:
\mathsf {isWeaklyConstant}(\mathsf {clean}^{h_A}_{x,y})
\\
&
\mathsf {cleanIsWeaklyConstant}_{x,y}~p~q :\equiv
\mathsf {act}_{\lambda r\mathpunct {.} \overline {\mathsf {repl}_{x,x}~\mathsf {refl}_x}\cdot r}
\bigl (\mathsf {replIsWeaklyConstant}_{x,y}~(h_Axy)\bigr )
\end {aligned}
Finally we can combine all this to verify Hedberg’s theorem:
\begin {aligned}
&
\mathsf {hedberg}:\mathsf {hasDecEq}(A)\to \mathsf {isSet}(A)
\\
&
\mathsf {hedberg}~h_A~x~y~p~q
:\equiv
\\
&\begin {array}{l}
\overline {\mathsf {cleanIsIdentity}_{h_A}~x~y~p}
\\
{}\cdot
\mathsf {cleanIsWeaklyConstant}^{h_A}_{x,y}~p~q
\\
{}\cdot
\mathsf {cleanIsIdentity}_{h_A}~x~y~q
\end {array}
\end {aligned}