2
$\begingroup$

Consider the intensional Martin-Löf type theory without axiom of choice or the law of excluded middle.

Let $A:U_0$ be a type and $B:A\to U_0$ be a function such that $\Sigma_{a:A}(B(a)\to 0)$is inhabited. Then $W_{a:A}B(a)$ is inhabited and so $(W_{a:A}B(a)\to 0)\to 0$ is inhabited. As an inhabited proposition $(W_{a:A}B(a)\to 0)\to 0$ has only one term in normal form. What is that term?

$\endgroup$
2
$\begingroup$

As an inhabited proposition $(W_{a:A}B(a)\to 0)\to 0$ has only one term in normal form.

First, without function extensionality, this type cannot be proven to be propositional. Second, propositional types do not necessarily have unique normal forms. Normal forms are up to $\beta\eta$ rules, not propositional equality.

$0 \to 0$ has infinitely many normal inhabitants. Listing a few:

$$\lambda\,x. x$$ $$\lambda\,x. \text{0-elim}\,x$$ $$\lambda\,x. \text{0-elim}\,(\text{0-elim}\,x)$$

Similarly, for any inhabited $A$, $(A \to 0) \to 0$ has infinitely many normal inhabitants.

$\endgroup$
4
  • $\begingroup$ Is there a way to decidably simplify the eliminator for the empty type? $\endgroup$ – user61651 Mar 19 at 8:28
  • $\begingroup$ Generally no. The strongest type theory where this is known to be possible is simple type theory with finite sums and products. As soon as you have natural numbers, normalizing modulo $\eta$-conversion for the empty type is undecidable. $\endgroup$ – András Kovács Mar 19 at 8:35
  • $\begingroup$ Is it correct that if a type is shown to be a proposition in a type theory with no non-computational axioms then there is a unique normal form? Because for closed terms propositional equality coincides with judgmental equality right? $\endgroup$ – user61651 Mar 19 at 9:25
  • $\begingroup$ @einzwein that's true in plain intensional MLTT, where the provably propositional closed types are pretty much just various products of the unit type. These all have definitionally unique inhabitants. With function extensionality, it's not true; e.g. $0 \to 0$ has inhabitants which are propositionally but not definitionally unique. $\endgroup$ – András Kovács Mar 19 at 10:47

Your Answer

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