Is there an explicit type $T$ in Martin-Löf type theory such that $(T\to \mathbf{0})\to\mathbf{0}$ has an explicit closed term and $T$ can be shown externally to not have closed terms?
1 Answer
Sure. Take any $A$ type which cannot be proven or disproven in MLTT, necessarily by some external argument. Then $A \lor \lnot A$ is not provable but $\lnot (\lnot (A \lor \lnot A))$ is provable, because this is an intuitionistic tautology for all $A$. Reminder: $\lnot A$ is defined as $A \to \mathbf{0}$.
Some examples for types whose inhabitation is independent from basic intuitionistic MLTT:
- Function extensionality
- Uniqueness of identity proofs
- Parametricity (for given types)
- Law of excluded middle
-
-
$\begingroup$ Let $A$ be one of my examples, then take $A \lor \lnot A$ for your $T$. $\endgroup$ Jun 12, 2021 at 19:39