"Upon This Quote I Will Build My Church Thesis"

The internal Church thesis (CT) is a logical principle stating that one can associate to any function 𝑓 : N → N a concrete code, in some Turing-complete language, that computes 𝑓 . While the compatibility of CT in simpler systems has been long known, its compatibility with dependent type theory is still an open question.

In this paper, we answer this question positively. We define "MLTT", a type theory extending MLTT with quote operators in which CT is derivable. We furthermore prove that "MLTT" is consistent, strongly normalizing and enjoys canonicity using a rather standard logical relation model. All the results in this paper have been mechanized in Coq 1 .