12
$\begingroup$

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?

$\endgroup$
12
$\begingroup$

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.

$\endgroup$
  • 5
    $\begingroup$ 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. $\endgroup$ – gallais Mar 13 '17 at 13:13
  • 1
    $\begingroup$ 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. $\endgroup$ – Mike Shulman Sep 4 '18 at 3:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.