  We prove consistency of intensional Martin-L\"of type theory (MLTT) with
formal Church's thesis (CT), which was open for at least fifteen years. The
difficulty in proving the consistency is that a standard method of
realizability \`{a} la Kleene does not work for the consistency, though it
validates CT, as it does not model MLTT; specifically, the realizability does
not validate MLTT's congruence rule on pi-types (known as the $\xi$-rule). We
overcome this point and prove the consistency by novel realizability \`{a} la
game semantics, which is based on the author's previous work.
