# Does the Law of Excluded Middle imply the Axiom K in Martin-Löf's Intensional Type Theory?

So I've been wondering if the Law of Excluded Middle (LEM) implies the so-called Axiom K in Martin-Löf's Intensional Type Theory. The Axiom K states that $$\Pi_{A : Type} \Pi_{x : A} \Pi_{p : \text{Id}(x,x)}, \text{Id}(p,\text{refl}_x)$$ In fact, I've been trying to prove the more general statement that $$\Pi_{A : Type} \Pi_{x, y : A} \Pi_{p,q : \text{Id}(x,y)}, \text{Id}(p,q)$$ but after reducing $q$ to $\text{refl}_x$ by equality-induction I am stuck into the first problem. I also tried to proceed by contradiction, but it doesn't seem to work..

Is this provable at all?

Yes, LEM implies K. See HoTT book Theorem 7.2.5, known as Hedberg's theorem, which shows that any type with decidable equality satisfies axiom $K$. If we assume excluded middle, all types have decidable equality.

Your second principle is known as UIP or Uniqueness of Identity Proofs. It is equivalent to Axiom K, see Theorem 7.2.1 in the HoTT book (just scroll up from 7.2.5 by one page). Neither of these can be derived in Martin-Löf intensional type theory, by a famous result of Thomas Streicher and Martin Hofmann.

• I'll take this opportunity to mention Alan Schmitt's elegant proof which clearly highlights the key ingredient: the ability, given an equality proof, to produce a canonical one. – gallais Mar 13 '17 at 13:13
• However, it is also worth noting that, as also pointed in the HoTT Book, there is a weaker form of "LEM" that doesn't imply K and is arguably what mathematicians really mean by LEM, namely LEM restricted to subsingleton types. – Mike Shulman Sep 4 '18 at 3:53