<p>Yes, LEM implies K. See <a href="https://books.google.si/books?id=LkDUKMv3yp0C&amp;lpg=PP1&amp;pg=PA224#v=onepage&amp;q&amp;f=false" rel="noreferrer">HoTT book Theorem 7.2.5</a>, 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.</p>

<p>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 href="https://homotopytypetheory.org/references/hofmann-streicher-the-groupoid-interpretation-of-type-theory/" rel="noreferrer">a famous result of Thomas Streicher and Martin Hofmann</a>. </p>

CC BY-SA 3.0
2017-03-13T13:13:03.023Z
I'll take this opportunity to mention [Alan Schmitt's elegant proof](https://sympa.inria.fr/sympa/arc/coq-club/2016-09/msg00064.html) which clearly highlights the key ingredient: the ability, given an equality proof, to produce a canonical one.
gallais
CC BY-SA 4.0
2018-09-04T03:53:07.160Z
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
CC BY-SA 3.0
2017-03-13T10:05:44.480Z
2017-03-13T10:11:02.887Z
2017-03-13T10:11:02.887Z
Andrej Bauer
<p>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..</p>

<p>Is this provable at all?</p>

<lo.logic><type-theory><lambda-calculus>
Does the Law of Excluded Middle imply the Axiom K in Martin-Löf's Intensional Type Theory?
StudentType
# Does the Law of Excluded Middle imply the Axiom K in Martin-Löf's Intensional Type Theory?

(Asked by: username_0 on 2017-03-13)

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?

**Tags:** lo.logic, type-theory, lambda-calculus


---

## 1 answers

### Answer by username_1 on 2017-03-13. Score: 13 | Accepted answer

Yes, LEM implies K. See [HoTT book Theorem 7.2.5](https://books.google.si/books?id=LkDUKMv3yp0C&lpg=PP1&pg=PA224#v=onepage&q&f=false), 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](https://homotopytypetheory.org/references/hofmann-streicher-the-groupoid-interpretation-of-type-theory/).

> **Comments:**
> **username_2**: I'll take this opportunity to mention [Alan Schmitt's elegant proof](https://sympa.inria.fr/sympa/arc/coq-club/2016-09/msg00064.html) which clearly highlights the key ingredient: the ability, given an equality proof, to produce a canonical one.  
> **username_3**: 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.  

---

