"Church's thesis" ($\mathsf{ CT}$) as an axiom in constructive logic states that every total function of type $\mathbb{ N} \to \mathbb{ N}$ is computable, i.e. definable in a model of computation. $\mathsf{ CT}$ is inconsistent in both classical mathematics and in Brouwer's intuitionism since it contradicts Weak K\"onig's Lemma and the fan theorem, respectively. Recently, $\mathsf{ CT}$ was proved consistent for (univalent) constructive type theory. Since neither Weak K\"onig's Lemma nor the fan theorem are a consequence of just logical axioms or just choice-like axioms assumed in constructive logic, it seems likely that $\mathsf{ CT}$ is inconsistent only with a combination of classical logic and choice axioms. We study consequences of $\mathsf{ CT}$ and its relation to several classes of axioms in Coq's type theory, a constructive type theory with a universe of propositions which does neither prove classical logical axioms nor strong choice axioms. We thereby provide a partial answer to the question which axioms may preserve computational intuitions inherent to type theory, and which certainly do not. The paper can also be read as a broad survey of axioms in type theory, with all results mechanised in the Coq proof assistant.
Categories: cs.LO