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