The "Under false pretenses" page concludes with a discussion of the "eta for $0$" rule in dependent type theory, saying
we would first need to decide whether the type of any variable in scope is or can be converted to $0$, which is not in general decidable.
This is not true -- definitional equality is (hopefully) decidable, and there are only finitely many variables in scope!
The issue is instead that the same reasoning holds not just for a variable x that's in scope, but for any term M that can be built using the variables in scope. So $\mathsf{true} \equiv \mathsf{false}$ iff the context is inconsistent (i.e. $\Gamma \vdash M : 0$ for a term $M$), which is not decidable.
The "Under false pretenses" page concludes with a discussion of the "eta for$0$ " rule in dependent type theory, saying
This is not true -- definitional equality is (hopefully) decidable, and there are only finitely many variables in scope!
The issue is instead that the same reasoning holds not just for a variable$\mathsf{true} \equiv \mathsf{false}$ iff the context is inconsistent (i.e. $\Gamma \vdash M : 0$ for a term $M$ ), which is not decidable.
xthat's in scope, but for any termMthat can be built using the variables in scope. So