0012
More path calculations
Posted at 20:56 on 21 September 2020, and revised at 10:15 on 22 September 2020
Continuing 0011, there are a couple more important theorems that can be proved with similar path calculations.
The first one is Hedberg’s theorem: if a type has decidable equality, then it is a set.
Or formally:
A useful observation here is that having decidable equality implies
where is propositional truncation (with as its constructor).
Intuitively, having decidable equality means that for every we can produce an inhabitant or prove that the type is uninhabited, so if we know in advance that is inhabited (that is, we have ), then we can definitely produce an inhabitant.
Type is a conditional version of , and we can largely repeat the argument in 0011 to create the equality structure required by .
Let be a function of Type .
Again attempting to relate and , we can derive
This is an equality between functions, which implies that applying both sides to the same argument yields the same result:
To proceed, we need to figure out how the transportation works.
The transportation has type
That is, it needs to produce a function of type from a function of type , and there seems to be only one sensible way: given an argument of type , we transport it backwards along to get an argument of type , which is fed to the given function, producing a result of type , and then we transport the result along to get the final result of type .
So we can rewrite the left-hand side of the equation and get
Here the transportation is the familiar one between equality types sharing the same base point, so we rewrite the transportation,
move to the right-hand side,
and substitute for and for :
The exact inhabitant produced on the right-hand side depends on and but not (since the third argument of is truncated), so for any , we have
completing the proof.
Note that Type is both sufficient (as shown above) and necessary for being a set.
Sufficiency is shown above, and necessity is straightforward: being a set means that the equality types on are all mere propositions, so we can just eliminate any given with the equality type itself as the target type.
The second theorem says that the unconstrained law of excluded middle is incompatible with univalence, that is,
if the universe is univalent.
The same observation made at the beginning of the proof of Hedberg’s theorem is also useful here: the law of excluded middle implies
that is, from every inhabited type we can choose an element.
Again, a function of Type preserves equality, which in this case implies that the function must make its choice for each type stably even when the elements of the type are permuted because univalence gives us the ability to permute the elements of a type by supplying an automorphism as an equivalence, but such choices are impossible.
Technically, we start with a function of Type , which preserves equality as before:
Again this is an equation on functions, which should map equal arguments to equal results:
The transportation is one between functions, and hence can be expanded to transportations of arguments and results as before:
Since the second argument of is irrelevant, what this says is that the element chosen from by , when transported along , should be the same as the element chosen from by .
If we allow non-trivial transportation when and are the same, then the equation will lead to a contradiction, but this non-trivial transportation is exactly one of the things univalence can give us.
Concretely, substitute for both and , the equality manufactured by univalence from the bijective function for , and an arbitrary element — say — for , and we’ll get
Rewriting the inner to just (which is ok since any two elements of a truncated type are equal) and observing that the outer is just applying the function , we get
which is clearly contradictory since doesn’t have a fixed point.