Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
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?
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.
