7.2 Uniqueness of identity proofs and Hedbergâs theorem
In §3.1 (http://planetmath.org/31setsandntypes) we defined a type to be a set if for all and we have . 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 -type in the sense of the previous section. Here is another equivalent characterization, involving Streicher’s “Axiom K” :
A type is a set if and only if it satisfies Axiom K: for all and we have .
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.
Suppose is a reflexive mere relation on a type implying identity. Then is a set, and is equivalent to for all .
Let witness reflexivity of , and let be a witness that implies identity. Note first that the two statements in the theorem are equivalent. For on one hand, if is a set, then is a mere proposition, and since it is logically equivalent to the mere proposition by hypothesis, it must also be equivalent to it. On the other hand, if is equivalent to , then like the latter it is a mere proposition for all , and hence is a set.
We give two proofs of this theorem. The first shows directly that is a set; the second shows directly that .
First proof: we show that is a set. The idea is the same as that of Lemma 3.3.4 (http://planetmath.org/33merepropositions#Thmprelem3): the function must be continuous in its arguments and . However, it is slightly more notationally complicated because we have to deal with the additional argument of type .
Firstly, for any and , consider . This is a dependent path from to itself. Since is still a function , by Lemma 2.9.6 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#Thmprelem1) this yields for any 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 , since both lie in the mere proposition . Thus, substituting , we obtain
By cancellation, . So satisfies Axiom K, and hence is a set.
Second proof: we show that each is an equivalence. By Theorem 4.7.7 (http://planetmath.org/47closurepropertiesofequivalences#Thmprethm4), it suffices to show that 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 . It remains to show, for every and every that
But since is a mere proposition, by Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1) it suffices to show that , which we get from . ∎
If a type has the property that for any , then 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 is said to have decidable equality if for all we have
This is a very strong condition: it says that a path can be chosen, when it exists, continuously (or computably, or functorially) in and . This turns out to imply that is a set, by way of Theorem 7.2.2 (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem#Thmprethm2) and the following lemma.
For any type we have .
Suppose . We have two cases to consider. If is for some , then we have the constant function which maps everything to . If is for some , we have for every . Hence we may use ex falso quodlibet, that is , to obtain an element of for any . ∎
Theorem 7.2.5 (Hedberg).
If has decidable equality, then is a set.
If has decidable equality, it follows that for any . 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 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.
The type of natural numbers has decidable equality, and hence is a set.
Let be given; we proceed by induction on and case analysis on to prove . If and , we take . If and , then by (2.13.2) (http://planetmath.org/213naturalnumbers#S0.E1) we get .
For the inductive step, let . If , we use (2.13.2) (http://planetmath.org/213naturalnumbers#S0.E1) again. Finally, if , the inductive hypothesis gives . In the first case, if , then . And in the second case, (2.13.3) (http://planetmath.org/213naturalnumbers#S0.E2) yields . ∎
Although Hedberg’s theorem appears rather special to sets (-types), “Axiom K” generalizes naturally to -types. Note that the ordinary Axiom K (as a property of a type ) states that for all , the loop space (see Definition 2.1.8 (http://planetmath.org/21typesarehighergroupoids#Thmpredefn2)) is contractible. Since is always inhabited (by ), this is equivalent to its being a mere proposition (a -type). Since , this suggests the following generalization.
For any , a type is an -type if and only if for all , the type is an -type.
Before proving this, we prove an auxiliary lemma:
Given and . If, given any inhabitant of it follows that is an -type, then is an -type.
Let be the given map. We need to show that for any , the type is an -type. But then shows that is an -type, hence all its path spaces are -types. ∎
Proof of Theorem 7.2.7 (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem#Thmprethm5).
The “only if” direction is obvious, since . Conversely, in order to show that is an -type, we need to show that for any , the type is an -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 , in which case it follows from the assumption that is an -type. ∎
By induction and some slightly clever whiskering, we can obtain a generalization of the K property to .
For every , a type is an -type if and only if is contractible for all .
Recalling that , the case is http://planetmath.org/node/87838Exercise 3.5. The case is Theorem 7.2.1 (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem#Thmprethm1). Now we use induction; suppose the statement holds for . By Theorem 7.2.7 (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem#Thmprethm5), is an -type iff is an -type for all . By the inductive hypothesis, the latter is equivalent to saying that is contractible for all .
Since , and , it will suffice to show that is equal to , in the type of pointed types. For this, it suffices to give an equivalence
which carries the basepoint to the basepoint . For , define to be the following composite:
where the path labeled “” is actually . Then 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 is the canonical equality. And it is evident that . ∎
- 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|