More path calculations
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:
$$ \Pi(A : \mathcal U)\ (\Pi(x\ y : A)\ (x =_A y) + \neg (x =_A y)) \to \mathsf{isSet}\ A $$
A useful observation here is that $A$ having decidable equality implies
\begin{equation} \Pi(x\ y : A)\ \| x =_A y \| \to x =_A y \label{type:conditionally-propositional} \end{equation}
where $\|\_\|$ is propositional truncation (with $|\_|$ as its constructor). Intuitively, having decidable equality means that for every $x =_A y$ we can produce an inhabitant or prove that the type is uninhabited, so if we know in advance that $x =_A y$ is inhabited (that is, we have $\| x =_A y \|$), then we can definitely produce an inhabitant. Type \ref{type:conditionally-propositional} is a conditional version of $\mathsf{isProp}$, and we can largely repeat the argument in 0011 to create the equality structure required by $\mathsf{isSet}\ A$. Let $f$ be a function of Type \ref{type:conditionally-propositional}. Again attempting to relate $f\ x\ z$ and $f\ x\ y$, we can derive
$$ \Pi(x\ z\ y : A)\ \Pi(p : z =_A y)\ p_*(f\ x\ z) = f\ x\ y $$
This is an equality between functions, which implies that applying both sides to the same argument yields the same result:
$$ \Pi(x\ z\ y : A)\ \Pi(p : z =_A y)\ \Pi(q : \| x =_A y \|)\ p_*(f\ x\ z)\ q = f\ x\ y\ q $$
To proceed, we need to figure out how the transportation $p_*$ works. The transportation has type
$$ p_* : (\| x =_A z \| \to x =_A z) \to (\| x =_A y \| \to x =_A y) $$ That is, it needs to produce a function of type $\| x =_A y \| \to x =_A y$ from a function of type $\| x =_A z \| \to x =_A z$, and there seems to be only one sensible way: given an argument of type $\| x =_A y \|$, we transport it backwards along $p^{-1}$ to get an argument of type $\| x =_A z \|$, which is fed to the given function, producing a result of type $x =_A z$, and then we transport the result along $p$ to get the final result of type $x =_A y$. So we can rewrite the left-hand side of the equation and get
$$ \Pi(x\ z\ y : A)\ \Pi(p : z =_A y)\ \Pi(q : \| x =_A y \|)\ p_*(f\ x\ z\ (p^{-1}_*\ q)) = f\ x\ y\ q $$
Here the transportation $p^*$ is the familiar one between equality types sharing the same base point, so we rewrite the transportation,
$$ \Pi(x\ z\ y : A)\ \Pi(p : z =_A y)\ \Pi(q : \| x =_A y \|)\ f\ x\ z\ (p^{-1}_*\ q) \cdot p = f\ x\ y\ q $$
move $f\ x\ z\ (p^{-1}_*\ q)$ to the right-hand side,
$$ \Pi(x\ z\ y : A)\ \Pi(p : z =_A y)\ \Pi(q : \| x =_A y \|)\ p = (f\ x\ z\ (p^{-1}_*\ q))^{-1} \cdot f\ x\ y\ q $$
and substitute $x$ for $z$ and $|p|$ for $q$:
$$ \Pi(x\ y : A)\ \Pi(p : x =_A y)\ p = (f\ x\ x\ (p^{-1}_*\ |p|))^{-1} \cdot f\ x\ y\ |p| $$
The exact inhabitant produced on the right-hand side depends on $x$ and $y$ but not $p$ (since the third argument of $f$ is truncated), so for any $p$, $q : x =_A y$ we have
\begin{align*} & p \\ =~& (f\ x\ x\ (p^{-1}_*\ |p|))^{-1} \cdot f\ x\ y\ |p| \\ =~& (f\ x\ x\ (q^{-1}_*\ |q|))^{-1} \cdot f\ x\ y\ |q| \\ =~& q \end{align*}
completing the proof. Note that Type \ref{type:conditionally-propositional} is both sufficient (as shown above) and necessary for $A$ being a set. Sufficiency is shown above, and necessity is straightforward: $A$ being a set means that the equality types on $A$ are all mere propositions, so we can just eliminate any given $\| x =_A y \|$ with the equality type $x =_A y$ itself as the target type.
The second theorem says that the unconstrained law of excluded middle is incompatible with univalence, that is,
$$ \neg \Pi(A : \mathcal U)\ A + \neg A $$
if the universe $\mathcal U$ 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
\begin{equation} \Pi(A : \mathcal U)\ \| A \| \to A \label{type:choice} \end{equation}
that is, from every inhabited type $A$ we can choose an element. Again, a function of Type \ref{type:choice} 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 $f$ of Type \ref{type:choice}, which preserves equality as before:
$$ \Pi(A\ B : \mathcal U)\ \Pi(p : A =_{\mathcal U} B)\ p_*(f\ A) = f\ B $$
Again this is an equation on functions, which should map equal arguments to equal results:
$$ \Pi(A\ B : \mathcal U)\ \Pi(p : A =_{\mathcal U} B)\ \Pi(b : \| B \|)\ p_*(f\ A)\ b = f\ B\ b $$
The transportation $p_* : (\| A \| \to A) \to (\| B \| \to B)$ is one between functions, and hence can be expanded to transportations of arguments and results as before:
$$ \Pi(A\ B : \mathcal U)\ \Pi(p : A =_{\mathcal U} B)\ \Pi(b : \| B \|)\ p_*(f\ A\ (p^{-1}_*\ b)) = f\ B\ b $$
Since the second argument of $f$ is irrelevant, what this says is that the element chosen from $A$ by $f$, when transported along $p$, should be the same as the element chosen from $B$ by $f$. If we allow non-trivial transportation when $A$ and $B$ 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 $\mathsf{Bool}$ for both $A$ and $B$, the equality $\mathsf{ua}(\mathsf{not})$ manufactured by univalence from the bijective function $\mathsf{not} : \mathsf{Bool} \to \mathsf{Bool}$ for $p$, and an arbitrary element — say $|\mathsf{true}|$ — for $b$, and we’ll get
$$ \mathsf{ua}(\mathsf{not})_*(f\ \mathsf{Bool}\ (\mathsf{ua}(\mathsf{not})^{-1}_*\ |\mathsf{true}|)) = f\ \mathsf{Bool}\ |\mathsf{true}| $$
Rewriting the inner $\mathsf{ua}(\mathsf{not})^{-1}_*\ |\mathsf{true}|$ to just $|\mathsf{true}|$ (which is ok since any two elements of a truncated type are equal) and observing that the outer $\mathsf{ua}(\mathsf{not})_* : \mathsf{Bool} \to \mathsf{Bool}$ is just applying the function $\mathsf{not}$, we get
$$ \mathsf{not}\ (f\ \mathsf{Bool}\ |\mathsf{true}|) = f\ \mathsf{Bool}\ |\mathsf{true}| $$
which is clearly contradictory since $\mathsf{not}$ doesn’t have a fixed point.
