# 7.2 Uniqueness of identity proofs and Hedbergâs theorem

In §3.1 (http://planetmath.org/31setsandntypes) we defined a type $X$ to be a set if for all $x,y:X$ and $p,q:x=_{X}y$ we have $p=q$. In conventional type theory  , this property goes by the name of . We have seen also that it is equivalent      to being a $0$-type in the sense of the previous section      . Here is another equivalent characterization  , involving Streicher’s “Axiom K” :

###### Theorem 7.2.1.

A type $X$ is a set if and only if it satisfies Axiom K: for all $x:X$ and $p:(x=_{A}x)$ we have $p=\mathsf{refl}_{x}$.

###### Proof.

Clearly Axiom K is a special case of UIP. Conversely, if $X$ satisfies Axiom K, let $x,y:X$ and $p,q:(x=y)$; we want to show $p=q$. But induction  on $q$ reduces this goal precisely to Axiom K. ∎

We stress that we are not assuming UIP or the K principle as axioms! They are simply properties which a particular type may or may not satisfy (which are equivalent to being a set). Recall from Example 3.1.9 (http://planetmath.org/31setsandntypes#Thmpreeg6) that not all types are sets.

###### Theorem 7.2.2.

Suppose $R$ is a reflexive   mere relation on a type $X$ implying identity. Then $X$ is a set, and $R(x,y)$ is equivalent to $x=_{X}y$ for all $x,y:X$.

###### Proof.

Let $\rho:\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{% (x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{% \prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x% :X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}R(x,x)$ witness reflexivity of $R$, and let $f:\mathchoice{\prod_{x,y:X}\,}{\mathchoice{{\textstyle\prod_{(x,y:X)}}}{\prod_% {(x,y:X)}}{\prod_{(x,y:X)}}{\prod_{(x,y:X)}}}{\mathchoice{{\textstyle\prod_{(x% ,y:X)}}}{\prod_{(x,y:X)}}{\prod_{(x,y:X)}}{\prod_{(x,y:X)}}}{\mathchoice{{% \textstyle\prod_{(x,y:X)}}}{\prod_{(x,y:X)}}{\prod_{(x,y:X)}}{\prod_{(x,y:X)}}% }R(x,y)\to(x=_{X}y)$ be a witness that $R$ implies identity. Note first that the two statements in the theorem are equivalent. For on one hand, if $X$ is a set, then $x=_{X}y$ is a mere proposition, and since it is logically equivalent to the mere proposition $R(x,y)$ by hypothesis   , it must also be equivalent to it. On the other hand, if $x=_{X}y$ is equivalent to $R(x,y)$, then like the latter it is a mere proposition for all $x,y:X$, and hence $X$ is a set.

We give two proofs of this theorem. The first shows directly that $X$ is a set; the second shows directly that $R(x,y)\simeq(x=y)$.

First proof: we show that $X$ is a set. The idea is the same as that of Lemma 3.3.4 (http://planetmath.org/33merepropositions#Thmprelem3): the function $f$ must be continuous  in its arguments $x$ and $y$. However, it is slightly more notationally complicated because we have to deal with the additional argument of type $R(x,y)$.

Firstly, for any $x:X$ and $p:x=_{X}x$, consider $\mathsf{apd}_{f(x)}(p)$. This is a dependent path from $f(x,x)$ to itself. Since $f(x,x)$ is still a function $R(x,x)\to(x=_{X}y)$, by Lemma 2.9.6 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#Thmprelem1) this yields for any $r:R(x,x)$ a path

 ${p}_{*}\mathopen{}\left({f(x,x,r)}\right)\mathclose{}=f(x,x,{p}_{*}\mathopen{}% \left({r}\right)\mathclose{}).$

On the left-hand side, we have transport in an identity type, which is concatenation. And on the right-hand side, we have ${p}_{*}\mathopen{}\left({r}\right)\mathclose{}=r$, since both lie in the mere proposition $R(x,x)$. Thus, substituting $r:\!\!\equiv\rho(x)$, we obtain

 $f(x,x,\rho(x))\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot% }}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}p=f(x,x,\rho(x)).$

By cancellation, $p=\mathsf{refl}_{x}$. So $X$ satisfies Axiom K, and hence is a set.

Second proof: we show that each $f(x,y):R(x,y)\to x=_{X}y$ is an equivalence. By Theorem 4.7.7 (http://planetmath.org/47closurepropertiesofequivalences#Thmprethm4), it suffices to show that $f$ induces an equivalence of total spaces:

 $\Bigl{(}\mathchoice{\sum_{y:X}\,}{\mathchoice{{\textstyle\sum_{(y:X)}}}{\sum_{% (y:X)}}{\sum_{(y:X)}}{\sum_{(y:X)}}}{\mathchoice{{\textstyle\sum_{(y:X)}}}{% \sum_{(y:X)}}{\sum_{(y:X)}}{\sum_{(y:X)}}}{\mathchoice{{\textstyle\sum_{(y:X)}% }}{\sum_{(y:X)}}{\sum_{(y:X)}}{\sum_{(y:X)}}}R(x,y)\Bigr{)}\simeq\Bigl{(}% \mathchoice{\sum_{y:X}\,}{\mathchoice{{\textstyle\sum_{(y:X)}}}{\sum_{(y:X)}}{% \sum_{(y:X)}}{\sum_{(y:X)}}}{\mathchoice{{\textstyle\sum_{(y:X)}}}{\sum_{(y:X)% }}{\sum_{(y:X)}}{\sum_{(y:X)}}}{\mathchoice{{\textstyle\sum_{(y:X)}}}{\sum_{(y% :X)}}{\sum_{(y:X)}}{\sum_{(y:X)}}}x=_{X}y\Bigr{)}.$

By Lemma 3.11.8 (http://planetmath.org/311contractibility#Thmprelem5), the type on the right is contractible, so it suffices to show that the type on the left is contractible. As the center of contraction we take the pair ${\mathopen{}(x,\rho(x))\mathclose{}}$. It remains to show, for every ${y:X}$ and every ${H:R(x,y)}$ that

 ${\mathopen{}(x,\rho(x))\mathclose{}}={\mathopen{}(y,H)\mathclose{}}.$

But since $R(x,y)$ is a mere proposition, by Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1) it suffices to show that $x=_{X}y$, which we get from $f(H)$. ∎

###### Corollary 7.2.3.

If a type $X$ has the property that $\neg\neg(x=y)\to(x=y)$ for any $x,y:X$, then $X$ is a set.

Another convenient way to show that a type is a set is the following. Recall from §3.4 (http://planetmath.org/34classicalvsintuitionisticlogic) that a type $X$ is said to have decidable equality if for all $x,y:X$ we have

 $(x=_{X}y)+\neg(x=_{X}y).$

This is a very strong condition: it says that a path $x=y$ can be chosen, when it exists, continuously (or computably, or functorially) in $x$ and $y$. This turns out to imply that $X$ is a set, by way of Theorem 7.2.2 (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem#Thmprethm2) and the following lemma.

###### Lemma 7.2.4.

For any type $A$ we have $(A+\neg A)\to(\neg\neg A\to A)$.

###### Proof.

Suppose $x:A+\neg A$. We have two cases to consider. If $x$ is ${\mathsf{inl}}(a)$ for some $a:A$, then we have the constant function $\neg\neg A\to A$ which maps everything to $a$. If $x$ is ${\mathsf{inr}}(f)$ for some $t:\neg A$, we have $g(t):\mathbf{0}$ for every $g:\neg\neg A$. Hence we may use ex falso quodlibet, that is $\mathsf{rec}_{\mathbf{0}}$, to obtain an element of $A$ for any $g:\neg\neg A$. ∎

###### Theorem 7.2.5 (Hedberg).

If $X$ has decidable equality, then $X$ is a set.

###### Proof.

If $X$ has decidable equality, it follows that $\neg\neg(x=y)\to(x=y)$ for any $x,y:X$. Therefore, Hedberg’s theorem follows from Corollary 7.2.3 (http://planetmath.org/72UniquenessOfIdentityProofsAndHedbergsTheorem#Thmprecor1). ∎

There is, of course, a strong connection between this theorem and Corollary 3.2.7 (http://planetmath.org/32propositionsastypes#Thmprecor1). The statement $\mathsf{LEM}_{\infty}$ that is denied by Corollary 3.2.7 (http://planetmath.org/32propositionsastypes#Thmprecor1) clearly implies that every type has decidable equality, and hence is a set, which we know is not the case. Note that the consistent axiom $\mathsf{LEM}$ from §3.4 (http://planetmath.org/34classicalvsintuitionisticlogic) implies only that every type has merely decidable equality, i.e. that for any $A$ we have

 $\mathchoice{\prod_{a,b:A}\,}{\mathchoice{{\textstyle\prod_{(a,b:A)}}}{\prod_{(% a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{\textstyle\prod_{(a,b% :A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}}{\mathchoice{{% \textstyle\prod_{(a,b:A)}}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}{\prod_{(a,b:A)}}% }(\mathopen{}\left\|a=b\right\|\mathclose{}+\neg\mathopen{}\left\|a=b\right\|% \mathclose{}).$

As an example application of Theorem 7.2.5 (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem#Thmprethm3), recall that in Example 3.1.4 (http://planetmath.org/31setsandntypes#Thmpreeg3) we observed that $\mathbb{N}$ is a set, using our characterization of its equality types in §2.13 (http://planetmath.org/213naturalnumbers). A more traditional proof of this theorem uses only (2.13.2) (http://planetmath.org/213naturalnumbers#S0.E1) and (2.13.2) (http://planetmath.org/213naturalnumbers#S0.E2), rather than the full characterization of Theorem 2.13.1 (http://planetmath.org/213naturalnumbers#Thmprethm1), with Theorem 7.2.5 (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem#Thmprethm3) to fill in the blanks.

###### Proof.

Let $x,y:\mathbb{N}$ be given; we proceed by induction on $x$ and case analysis on $y$ to prove $(x=y)+\neg(x=y)$. If $x\equiv 0$ and $y\equiv 0$, we take ${\mathsf{inl}}(\mathsf{refl}(0))$. If $x\equiv 0$ and $y\equiv\mathsf{succ}(n)$, then by (2.13.2) (http://planetmath.org/213naturalnumbers#S0.E1) we get $\neg(0=\mathsf{succ}(n))$.

For the inductive step, let $x\equiv\mathsf{succ}(n)$. If $y\equiv 0$, we use (2.13.2) (http://planetmath.org/213naturalnumbers#S0.E1) again. Finally, if $y\equiv\mathsf{succ}(m)$, the inductive hypothesis gives $(m=n)+\neg(m=n)$. In the first case, if $p:m=n$, then ${\mathsf{succ}}\mathopen{}\left({p}\right)\mathclose{}:\mathsf{succ}(m)=% \mathsf{succ}(n)$. And in the second case, (2.13.3) (http://planetmath.org/213naturalnumbers#S0.E2) yields $\neg(\mathsf{succ}(m)=\mathsf{succ}(n))$. ∎

Although Hedberg’s theorem appears rather special to sets ($0$-types), “Axiom K” generalizes naturally to $n$-types. Note that the ordinary Axiom K (as a property of a type $X$) states that for all $x:X$, the loop space  $\Omega(X,x)$ (see Definition 2.1.8 (http://planetmath.org/21typesarehighergroupoids#Thmpredefn2)) is contractible. Since $\Omega(X,x)$ is always inhabited (by $\mathsf{refl}_{x}$), this is equivalent to its being a mere proposition (a $(-1)$-type). Since $0=(-1)+1$, this suggests the following generalization  .

###### Theorem 7.2.7.

For any $n\geq-1$, a type $X$ is an $(n+1)$-type if and only if for all $x:X$, the type $\Omega(X,x)$ is an $n$-type.

Before proving this, we prove an auxiliary lemma:

###### Lemma 7.2.8.

Given $n\geq-1$ and $X:\mathcal{U}$. If, given any inhabitant of $X$ it follows that $X$ is an $n$-type, then $X$ is an $n$-type.

###### Proof.

Let $f:X\to\mathsf{is}\mbox{-}{n}\mbox{-}\mathsf{type}(X)$ be the given map. We need to show that for any $x,x^{\prime}:X$, the type $x=x^{\prime}$ is an $(n-1)$-type. But then $f(x)$ shows that $X$ is an $n$-type, hence all its path spaces are $(n-1)$-types. ∎

###### Proof of Theorem 7.2.7 (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem#Thmprethm5).

The “only if” direction is obvious, since $\Omega(X,x):\!\!\equiv(x=_{X}x)$. Conversely, in order to show that $X$ is an $(n+1)$-type, we need to show that for any $x,x^{\prime}:X$, the type $x=x^{\prime}$ is an $n$-type. Following Lemma 7.2.8 (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem#Thmprelem2) it suffices to give a map

 $(x=x^{\prime})\to\mathsf{is}\mbox{-}{n}\mbox{-}\mathsf{type}(x=x^{\prime}).$

By path induction, it suffices to do this when $x\equiv x^{\prime}$, in which case it follows from the assumption  that $\Omega(X,x)$ is an $n$-type. ∎

By induction and some slightly clever whiskering, we can obtain a generalization of the K property to $n>0$.

###### Theorem 7.2.9.

For every $n\geq-1$, a type $A$ is an $n$-type if and only if $\Omega^{n+1}(A,a)$ is contractible for all $a:A$.

###### Proof.

Recalling that $\Omega^{0}(A,a)=(A,a)$, the case $n=-1$ is http://planetmath.org/node/87838Exercise 3.5. The case $n=0$ is Theorem 7.2.1 (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem#Thmprethm1). Now we use induction; suppose the statement holds for $n:\mathbb{N}$. By Theorem 7.2.7 (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem#Thmprethm5), $A$ is an $(n+1)$-type iff $\Omega(A,a)$ is an $n$-type for all $a:A$. By the inductive hypothesis, the latter is equivalent to saying that $\Omega^{n+1}(\Omega(A,a),p)$ is contractible for all $p:\Omega(A,a)$.

Since $\Omega^{n+2}(A,a):\!\!\equiv\Omega^{n+1}(\Omega(A,a),\mathsf{refl}_{a})$, and $\Omega^{n+1}=\Omega^{n}\circ\Omega$, it will suffice to show that $\Omega(\Omega(A,a),p)$ is equal to $\Omega(\Omega(A,a),\mathsf{refl}_{a})$, in the type $\mathcal{U}_{\bullet}$ of pointed types. For this, it suffices to give an equivalence

 $g:\Omega(\Omega(A,a),p)\simeq\Omega(\Omega(A,a),\mathsf{refl}_{a})$

which carries the basepoint $\mathsf{refl}_{p}$ to the basepoint $\mathsf{refl}_{\mathsf{refl}_{a}}$. For $q:p=p$, define $g(q):\mathsf{refl}_{a}=\mathsf{refl}_{a}$ to be the following composite:

 $\mathsf{refl}_{a}=p\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}\mathord{{p}^{-1}}\overset{q}{=}p% \mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}\mathord{{p}^{-1}}=\mathsf{refl}_{a},$

where the path labeled “$q$” is actually $\mathsf{ap}_{{\lambda}r.\,r\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathord{{p}^{-1}}}(q)$. Then $g$ is an equivalence because it is a composite of equivalences

 $(p=p)\xrightarrow{\mathsf{ap}_{{\lambda}r.\,r\mathchoice{\mathbin{\raisebox{2.% 15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathord{{p}^{-1}}}}(p% \mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}\mathord{{p}^{-1}}=p\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}\mathord{{p}^{-1}})\xrightarrow{i% \mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}-\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{% \mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}\mathord{{i}^{-1}}}(\mathsf{refl}_{a}=\mathsf{refl}_{a}).$

using Example 2.4.8 (http://planetmath.org/24homotopiesandequivalences#Thmpreeg2),Theorem 2.11.1 (http://planetmath.org/211identitytype#Thmprethm1), where $i:\mathsf{refl}_{a}=p\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}\mathord{{p}^{-1}}$ is the canonical equality. And it is evident that $g(\mathsf{refl}_{p})=\mathsf{refl}_{\mathsf{refl}_{a}}$. ∎

## References

• 1 Thomas Streicher. Investigations into intensional type theory, 1993. Habilitationsschrift,Ludwig-Maximilians-Universität München.
 Title 7.2 Uniqueness of identity proofs and Hedbergâs theorem \metatable