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=Xy we have p=q. In conventional type theoryPlanetmathPlanetmath, this property goes by the name of uniqueness of identityPlanetmathPlanetmathPlanetmathPlanetmath proofs (UIP). We have seen also that it is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to being a 0-type in the sense of the previous sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath. Here is another equivalent characterizationMathworldPlanetmath, 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:X and p:(x=Ax) we have p=reflx.


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 inductionMathworldPlanetmath 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 theoremMathworldPlanetmath is another useful way to show that types are sets.

Theorem 7.2.2.

Suppose R is a reflexiveMathworldPlanetmathPlanetmath mere relation on a type X implying identity. Then X is a set, and R(x,y) is equivalent to x=Xy for all x,y:X.


Let ρ:(x:X)R(x,x) witness reflexivity of R, and let f:(x,y:X)R(x,y)(x=Xy) 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=Xy is a mere proposition, and since it is logically equivalent to the mere proposition R(x,y) by hypothesisMathworldPlanetmathPlanetmath, it must also be equivalent to it. On the other hand, if x=Xy 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)(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 continuousPlanetmathPlanetmath 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=Xx, consider 𝖺𝗉𝖽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)(x=Xy), by Lemma 2.9.6 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#Thmprelem1) this yields for any r:R(x,x) a path


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


By cancellation, p=𝗋𝖾𝖿𝗅x. So X satisfies Axiom K, and hence is a set.

Second proof: we show that each f(x,y):R(x,y)x=Xy 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:


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 (x,ρ(x)). It remains to show, for every y:X and every H:R(x,y) that


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=Xy, which we get from f(H). ∎

Corollary 7.2.3.

If a type X has the property that ¬¬(x=y)(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


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+¬A)(¬¬AA).


Suppose x:A+¬A. We have two cases to consider. If x is 𝗂𝗇𝗅(a) for some a:A, then we have the constant function ¬¬AA which maps everything to a. If x is 𝗂𝗇𝗋(f) for some t:¬A, we have g(t):𝟎 for every g:¬¬A. Hence we may use ex falso quodlibet, that is 𝗋𝖾𝖼𝟎, to obtain an element of A for any g:¬¬A. ∎

Theorem 7.2.5 (Hedberg).

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


If X has decidable equality, it follows that ¬¬(x=y)(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 𝖫𝖤𝖬 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 𝖫𝖤𝖬 from §3.4 (http://planetmath.org/34classicalvsintuitionisticlogic) implies only that every type has merely decidable equality, i.e. that for any A we have


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

Theorem 7.2.6.

The type N of natural numbersMathworldPlanetmath has decidable equality, and hence is a set.


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

For the inductive step, let x𝗌𝗎𝖼𝖼(n). If y0, we use (2.13.2) (http://planetmath.org/213naturalnumbers#S0.E1) again. Finally, if y𝗌𝗎𝖼𝖼(m), the inductive hypothesis gives (m=n)+¬(m=n). In the first case, if p:m=n, then 𝗌𝗎𝖼𝖼(p):𝗌𝗎𝖼𝖼(m)=𝗌𝗎𝖼𝖼(n). And in the second case, (2.13.3) (http://planetmath.org/213naturalnumbers#S0.E2) yields ¬(𝗌𝗎𝖼𝖼(m)=𝗌𝗎𝖼𝖼(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 spaceMathworldPlanetmath Ω(X,x) (see Definition 2.1.8 (http://planetmath.org/21typesarehighergroupoids#Thmpredefn2)) is contractible. Since Ω(X,x) is always inhabited (by 𝗋𝖾𝖿𝗅x), this is equivalent to its being a mere proposition (a (-1)-type). Since 0=(-1)+1, this suggests the following generalizationPlanetmathPlanetmath.

Theorem 7.2.7.

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

Before proving this, we prove an auxiliary lemma:

Lemma 7.2.8.

Given n-1 and X:U. If, given any inhabitant of X it follows that X is an n-type, then X is an n-type.


Let f:X𝗂𝗌-n-𝗍𝗒𝗉𝖾(X) be the given map. We need to show that for any x,x:X, the type x=x 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 Ω(X,x):(x=Xx). Conversely, in order to show that X is an (n+1)-type, we need to show that for any x,x:X, the type x=x is an n-type. Following Lemma 7.2.8 (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem#Thmprelem2) it suffices to give a map


By path induction, it suffices to do this when xx, in which case it follows from the assumptionPlanetmathPlanetmath that Ω(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-1, a type A is an n-type if and only if Ωn+1(A,a) is contractible for all a:A.


Recalling that Ω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:. By Theorem 7.2.7 (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem#Thmprethm5), A is an (n+1)-type iff Ω(A,a) is an n-type for all a:A. By the inductive hypothesis, the latter is equivalent to saying that Ωn+1(Ω(A,a),p) is contractible for all p:Ω(A,a).

Since Ωn+2(A,a):Ωn+1(Ω(A,a),𝗋𝖾𝖿𝗅a), and Ωn+1=ΩnΩ, it will suffice to show that Ω(Ω(A,a),p) is equal to Ω(Ω(A,a),𝗋𝖾𝖿𝗅a), in the type 𝒰 of pointed types. For this, it suffices to give an equivalence


which carries the basepoint 𝗋𝖾𝖿𝗅p to the basepoint 𝗋𝖾𝖿𝗅𝗋𝖾𝖿𝗅a. For q:p=p, define g(q):𝗋𝖾𝖿𝗅a=𝗋𝖾𝖿𝗅a to be the following composite:


where the path labeled “q” is actually 𝖺𝗉λr.r\centerdotp-1(q). Then g is an equivalence because it is a composite of equivalences


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


  • 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