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.