‘Upon This Quote I Will Build My Church Thesis’

The internal Church thesis ( <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mi mathvariant="sans-serif">CT</mml:mi> </mml:math> ) is a logical principle stating that one can associate to any function <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mrow> <mml:mi>f</mml:mi> <mml:mspace width="0.2em"/> <mml:mo>:</mml:mo> <mml:mspace width="0.2em"/> <mml:mi mathvariant="double-struck">N</mml:mi> <mml:mo>→</mml:mo> <mml:mi mathvariant="double-struck">N</mml:mi> </mml:mrow> </mml:math> a concrete code, in some Turing-complete language, that computes <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mi>f</mml:mi> </mml:math> . While the compatibility of <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mi mathvariant="sans-serif">CT</mml:mi> </mml:math> 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 <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mrow> <mml:mo mathvariant="sans-serif">“</mml:mo> <mml:mi mathvariant="sans-serif">MLTT</mml:mi> <mml:mo mathvariant="sans-serif">”</mml:mo> </mml:mrow> </mml:math> , a type theory extending <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mi mathvariant="sans-serif">MLTT</mml:mi> </mml:math> with quote operators in which <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mi mathvariant="sans-serif">CT</mml:mi> </mml:math> is derivable. We furthermore prove that <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mrow> <mml:mo mathvariant="sans-serif">“</mml:mo> <mml:mi mathvariant="sans-serif">MLTT</mml:mi> <mml:mo mathvariant="sans-serif">”</mml:mo> </mml:mrow> </mml:math> 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. a