We work in homotopy type theory. Denote the propositional truncation of a type $A$ by $\|A\|$ and the function type between types $A$ and $B$ by $A \to B$.

Can you construct a term of the following type: $$ \prod_{A:U_0}\prod_{B:U_0} (\|A\| \to A) \times (\|B\| \to B) \to (\|A + B\| \to A + B) \quad? $$

  • $\begingroup$ Oh, sorry, I somehow misread the last $\mathrm{Fun}$ as $\simeq$. By the way, why aren't you writing $A \to B$ instead of $\mathrm{Fun}(A,B)$, as is standard? And propositional truncation should be LaTeXed as \|A\| to give you $\|A\|$ instead of $||A||$. $\endgroup$ Mar 13 at 6:58
  • $\begingroup$ @AndrejBauer can you associatively parse the arrow notation? I am a little unsure regarding that. $\endgroup$
    – user61651
    Mar 13 at 7:03
  • $\begingroup$ $A \to B \to C = A \to (B \to C)$ by convention. $\endgroup$ Mar 13 at 7:09
  • $\begingroup$ The coproduct $A + B$ in your type need not be inhabited (consider $A = B = 0$), so perhaps your title is a bit misleading. $\endgroup$ Mar 13 at 7:15
  • $\begingroup$ @AndrejBauer OK I changed the title. $\endgroup$
    – user61651
    Mar 13 at 7:23

We are going to show that in MLTT with propositional truncation the type $$\textstyle \prod_{A:U_0}\prod_{B:U_0} (\|A\| \to A) \times (\|B\| \to B) \to (\|A + B\| \to A + B) $$ has no inhabitants. Assume it did.

We shall work in a specific model of MLTT with propositional truncation, namely assemblies over number realizability. It is not too important what this model is precisely, except for the following facts:

  • there is an object of reals $\mathbb{R}$ in which
  • $\Pi (x : \mathbb{R}) \; \|(x < 1) + (x > 0)\|$, and
  • every map $\mathbb{R} \to \mathsf{bool}$ is constant.

Hoever, using the above type, we may inhabit $$\Pi(x : \mathbb{R}) \; \|x < 1\| + \|x > 0\|,$$ contradicting the fact that every map $\mathbb{R} \to \mathsf{bool}$ is constant. To do so, consider any $x : \mathbb{R}$ and instantiate $A = \|x < 1\|$ and $B = \|x > 1\|$ (and use the fact that $<$ maps into propositions).

  • $\begingroup$ So if it has no inhabitants is there an explicit term of the negation? $\endgroup$
    – user61651
    Mar 13 at 8:22
  • $\begingroup$ No. Because that would violate another model (classical set theory) in which your type is inhabited. $\endgroup$ Mar 13 at 8:33
  • $\begingroup$ This type is a much simpler witness of incompleteness than what is provided by Goedel's theorems. Curious. $\endgroup$
    – user61651
    Mar 13 at 8:39
  • 3
    $\begingroup$ That is a feature of intuitionistic logic. With fewer axioms (no excluded middle) it becomes easier to find undecided statements. The point of Gödel's theorems is not to give one particular undecided sentence, but to give a procedure for generating them. $\endgroup$ Mar 13 at 8:43

Your Answer

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