The internal Church thesis (CT) is a logical principle stating that any function f : N → N is computed by a concrete program in some Turing-complete language. CT has been widely used in constructive mathematics, most specifically in the Russian tradition. On the other side of the iron curtain, Martin-Loef Type Theory (MLTT) was designed as the modern embodiment of Bishop-style neutral mathematics. It should come as a surprise that the natural type-theoretic equivalent of CT was conjectured to be inconsistent with MLTT. In this talk, we will prove that this conjecture is false, by introducing “MLTT”, a consistent extension of MLTT with quoting primitives that implements CT in a computational way.