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 uniqueness of identity proofs (UIP).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” [1]:

Theorem 7.2.1.

A type $X$ is a set if and only if it satisfies Axiom K:for all $x\mathrm{:}X$ and $p\mathrm{:}\mathrm{(}x{\mathrm{=}}_{A}x\mathrm{)}$ we have $p\mathrm{=}{\mathrm{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.

The following theorem is another useful way to show that 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\mathit{}\mathrm{(}x\mathrm{,}y\mathrm{)}$ is equivalent to $x{\mathrm{=}}_{X}y$ for all $x\mathrm{,}y\mathrm{:}X$.

Proof.

Let $\rho :{\prod }_{(x:X)}R(x,x)$ witness reflexivity of $R$, and let $f:{\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 ${\mathrm{𝖺𝗉𝖽}}_{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_{*}\left(f(x,x,r)\right)=f(x,x,p_{*}\left(r\right)).$$

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

$$f(x,x,\rho (x))p=f(x,x,\rho (x)).$$

By cancellation, $p={\mathrm{𝗋𝖾𝖿𝗅}}_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:

$$\left(\sum _{y:X}R(x,y)\right)\simeq \left(\sum _{y:X}x{=}_{X}y\right).$$

By Lemma 3.11.8 (http://planetmath.org/311contractibility#Thmprelem5), the type on the right is contractible, so itsuffices to show that the type on the left is contractible. As the center ofcontraction we take the pair $(x,\rho (x))$. It remains to show, forevery $y:X$ and every $H:R(x,y)$ that

$$(x,\rho (x))=(y,H).$$

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 $\mathrm{\neg }\mathrm{\neg }\mathrm{(}x\mathrm{=}y\mathrm{)}\mathrm{\to }\mathrm{(}x\mathrm{=}y\mathrm{)}$ for any $x\mathrm{,}y\mathrm{:}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 equalityif for all $x,y:X$ we have

$$(x{=}_{X}y)+\mathrm{\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 $\mathrm{(}A\mathrm{+}\mathrm{\neg }A\mathrm{)}\mathrm{\to }\mathrm{(}\mathrm{\neg }\mathrm{\neg }A\mathrm{\to }A\mathrm{)}$.

Proof.

Suppose $x:A+\mathrm{\neg }A$. We have two cases to consider.If $x$ is $\mathrm{𝗂𝗇𝗅}(a)$ for some $a:A$, then we have the constant function $\mathrm{\neg }\mathrm{\neg }A\to A$ which maps everything to $a$. If $x$ is $\mathrm{𝗂𝗇𝗋}(f)$ for some $t:\mathrm{\neg }A$,we have $g(t):\mathrm{𝟎}$ for every $g:\mathrm{\neg }\mathrm{\neg }A$. Hence we may useex falso quodlibet, that is ${\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟎}}$, to obtain an element of $A$ for any $g:\mathrm{\neg }\mathrm{\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 $\mathrm{\neg }\mathrm{\neg }(x=y)\to (x=y)$ for any$x,y:X$. Therefore, Hedberg’s theorem follows fromCorollary 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 ${\mathrm{𝖫𝖤𝖬}}_{\mathrm{\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 $\mathrm{𝖫𝖤𝖬}$ from §3.4 (http://planetmath.org/34classicalvsintuitionisticlogic) implies only that every type has merely decidable equality, i.e. that for any $A$ we have

$$\prod _{a,b:A}(\parallel a=b\parallel +\mathrm{\neg }\parallel a=b\parallel ).$$

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

Theorem 7.2.6.

The type $\mathrm{N}$ of natural numbers has decidable equality, and hence is a set.

Proof.

Let $x,y:\mathbb{N}$ be given; we proceed by induction on $x$ and case analysis on $y$ to prove $(x=y)+\mathrm{\neg }(x=y)$.If $x\equiv 0$ and $y\equiv 0$, we take $\mathrm{𝗂𝗇𝗅}(\mathrm{𝗋𝖾𝖿𝗅}(0))$.If $x\equiv 0$ and $y\equiv \mathrm{𝗌𝗎𝖼𝖼}(n)$, then by (2.13.2) (http://planetmath.org/213naturalnumbers#S0.E1) we get $\mathrm{\neg }(0=\mathrm{𝗌𝗎𝖼𝖼}(n))$.

For the inductive step, let $x\equiv \mathrm{𝗌𝗎𝖼𝖼}(n)$.If $y\equiv 0$, we use (2.13.2) (http://planetmath.org/213naturalnumbers#S0.E1) again.Finally, if $y\equiv \mathrm{𝗌𝗎𝖼𝖼}(m)$, the inductive hypothesis gives $(m=n)+\mathrm{\neg }(m=n)$.In the first case, if $p:m=n$, then $\mathrm{𝗌𝗎𝖼𝖼}\left(p\right):\mathrm{𝗌𝗎𝖼𝖼}(m)=\mathrm{𝗌𝗎𝖼𝖼}(n)$.And in the second case, (2.13.3) (http://planetmath.org/213naturalnumbers#S0.E2) yields $\mathrm{\neg }(\mathrm{𝗌𝗎𝖼𝖼}(m)=\mathrm{𝗌𝗎𝖼𝖼}(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 $\mathrm{\Omega }(X,x)$ (see Definition 2.1.8 (http://planetmath.org/21typesarehighergroupoids#Thmpredefn2)) is contractible.Since $\mathrm{\Omega }(X,x)$ is always inhabited (by ${\mathrm{𝗋𝖾𝖿𝗅}}_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\mathrm{\ge }\mathrm{-}\mathrm{1}$, a type $X$ is an $\mathrm{(}n\mathrm{+}\mathrm{1}\mathrm{)}$-type if and only if for all $x\mathrm{:}X$, the type $\mathrm{\Omega }\mathit{}\mathrm{(}X\mathrm{,}x\mathrm{)}$ is an $n$-type.

Before proving this, we prove an auxiliary lemma:

Lemma 7.2.8.

Given $n\mathrm{\ge }\mathrm{-}\mathrm{1}$ and $X\mathrm{:}\mathrm{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 \mathrm{𝗂𝗌}\text{-}n\text{-}\mathrm{𝗍𝗒𝗉𝖾}(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 $\mathrm{\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 \mathrm{𝗂𝗌}\text{-}n\text{-}\mathrm{𝗍𝗒𝗉𝖾}(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 $\mathrm{\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\mathrm{\ge }\mathrm{-}\mathrm{1}$, a type $A$ is an $n$-type if and only if ${\mathrm{\Omega }}^{n\mathrm{+}\mathrm{1}}\mathit{}\mathrm{(}A\mathrm{,}a\mathrm{)}$ is contractible for all $a\mathrm{:}A$.

Proof.

Recalling that ${\mathrm{\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 $\mathrm{\Omega }(A,a)$ is an $n$-type for all $a:A$.By the inductive hypothesis, the latter is equivalent to saying that ${\mathrm{\Omega }}^{n+1}(\mathrm{\Omega }(A,a),p)$ is contractible for all $p:\mathrm{\Omega }(A,a)$.

Since ${\mathrm{\Omega }}^{n+2}(A,a):\equiv {\mathrm{\Omega }}^{n+1}(\mathrm{\Omega }(A,a),{\mathrm{𝗋𝖾𝖿𝗅}}_a)$, and ${\mathrm{\Omega }}^{n+1}={\mathrm{\Omega }}^n\circ \mathrm{\Omega }$, it will suffice to show that $\mathrm{\Omega }(\mathrm{\Omega }(A,a),p)$ is equal to $\mathrm{\Omega }(\mathrm{\Omega }(A,a),{\mathrm{𝗋𝖾𝖿𝗅}}_a)$, in the type ${𝒰}_{\bullet }$ of pointed types.For this, it suffices to give an equivalence

$$g:\mathrm{\Omega }(\mathrm{\Omega }(A,a),p)\simeq \mathrm{\Omega }(\mathrm{\Omega }(A,a),{\mathrm{𝗋𝖾𝖿𝗅}}_a)$$

which carries the basepoint ${\mathrm{𝗋𝖾𝖿𝗅}}_p$ to the basepoint ${\mathrm{𝗋𝖾𝖿𝗅}}_{{\mathrm{𝗋𝖾𝖿𝗅}}_a}$.For $q:p=p$, define $g(q):{\mathrm{𝗋𝖾𝖿𝗅}}_a={\mathrm{𝗋𝖾𝖿𝗅}}_a$ to be the following composite:

$${\mathrm{𝗋𝖾𝖿𝗅}}_a=p{p}^{-1}\stackrel{𝑞}{=}p{p}^{-1}={\mathrm{𝗋𝖾𝖿𝗅}}_a,$$

where the path labeled “$q$” is actually ${\mathrm{𝖺𝗉}}_{\lambda r.r{p}^{-1}}(q)$.Then $g$ is an equivalence because it is a composite of equivalences

$$(p=p)\stackrel{{\mathrm{𝖺𝗉}}_{\lambda r.r{p}^{-1}}}{\to }(p{p}^{-1}=p{p}^{-1})\stackrel{i-i^{-1}}{\to }({\mathrm{𝗋𝖾𝖿𝗅}}_a={\mathrm{𝗋𝖾𝖿𝗅}}_a).$$

using Example 2.4.8 (http://planetmath.org/24homotopiesandequivalences#Thmpreeg2),Theorem 2.11.1 (http://planetmath.org/211identitytype#Thmprethm1), where $i:{\mathrm{𝗋𝖾𝖿𝗅}}_a=p{p}^{-1}$ is the canonical equality.And it is evident that $g({\mathrm{𝗋𝖾𝖿𝗅}}_p)={\mathrm{𝗋𝖾𝖿𝗅}}_{{\mathrm{𝗋𝖾𝖿𝗅}}_a}$.∎