  "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.
