Context
The following question concerns plain Martin-Löf type theory, under a propositions-as-types interpretation: in particular, proposition simply means type and not mere proposition, and disjunction is interpreted as the usual sum type, and not its -1-truncation.
We can consistently add either an inhabitant of the type $\Pi P:\mathrm{Type}. P \vee \neg P$ or an inhabitant of its negation, the type $\neg \left(\Pi P:\mathrm{Type}. P \vee \neg P\right)$ to Martin-Löf type theory axiomatically. Indeed, the axioms of Homotopy Type Theory allow us to inhabit the latter type: this follows as an immediate corollary of Theorem 3.2.2. in the HoTT Book. The way each of these principles affects the logic is well-understood.
The question below aims to tease out the strength of the double negation of excluded middle, $\neg\neg \left(\Pi P:\mathrm{Type}. P \vee \neg P \right)$, as a logical principle.
Question
Let $\mathrm{\neg\neg LEM}$ denote the type $\neg\neg \left(\Pi P:\mathrm{Type}. P \vee \neg P\right)$.
What is the smallest term $t(X)$ in the Rieger-Nishimura lattice so that the type $(\neg\neg \mathrm{LEM}) \rightarrow \left(\Pi P : \mathrm{Type}. t(P)\right)$ is inhabited in Martin-Löf type theory?
In particular, does $\neg\neg \mathrm{LEM} \rightarrow \mathrm{LEM}$?
edit: The answer to the easy part is negative: MLTT does not prove $\neg\neg \mathrm{LEM} \rightarrow \mathrm{LEM}$. This is because MLTT + $(\Pi P: \mathrm{Type}_1. \neg P \vee \neg\neg P)$ clearly suffices to prove $\neg\neg \mathrm{LEM}$, but it nonetheless has models where $\mathrm{LEM}$ fails. This means that $[\top] \geq t(X) > [\neg X \vee \neg\neg X]$ in the Rieger-Nishimura lattice.