@JasonRute if $T$ is classical, than the church rule can't hold because $T$ will be able to show the existence of uncomputable functions. For example, PA proves "for all x there is a y such that y is the xth busy beaver number", in which case $e$ won't exist.

@JasonRute there are no conditions of $\phi$ other than there being a proof of $\forall x.\exists y. \phi(x,y)$. The reason CR can exist is that in constructive proofs can be turned into programs. The program is found by analyzing the proof, not by analyzing the formula $\phi$.

@JasonRute by "implement" I mean an actual piece of software. I am very confident that CR is correct in Agda and Coq. CR is correct in IZF, for example. But I don't know of any software for performing it automatically. (It is always computable for recursively enumerable theories.)

Is $\exists$ allowed te interpreted as $\Sigma$?

@AndrejBauer yeah that's fine. In a system with both, CR using either $\exists$ or $\Sigma$ works.

It was a trick question: From $t : \Pi (x : A) \Sigma (y : B) .\, \phi(x,y)$ we can get a closed term $f = \pi_1 \circ t : A \to B$ and a proof that it works, and we're done.

@AndrejBauer hmm, it's a very subtle issue but I think technically this approach would require $\eta$ to be an interpreter for $T$ terms, which I imagine is impossible to use for Gödelian/Tarskian reasons. $e$ is supposed to part of a discrete data structure, but $f$ is a function. The term underlying $f$ can be represented by a natural number, but turning it back into a function requires an interpreter.

You can use meta-programming features tu turn f into code (a discrete data structure). And since we're talking about a rule that only applies to sentences, we must go meta-level at some point.

Actually, how is $\eta$ supposed to work? If it's an interpreter for $T$ then there's a problem.

@AndrejBauer $\eta$ could just be an interpreter for Turing machines. That doesn't run into any logical issues (although there are probably more convenient numberings that also avoid logical issues).

It cannot be just that, or else you would introduce partial maps into your type theory.

@AndrejBauer okay so my notation was perhaps a bit misleading. $\eta$ should actually be thought of as a relation, not a function. This formulation of CT is more specific about this (and also applies to CR).

That makes more sense. My observation still stands: it's more productive to implement reflection, quoting and other meta-level techniques, and leave the actual comittment to CT (either as an axiom or as a rule) to people who want it.

OTH, people do care about the fact that every closed term of type $\mathbb{N} \to \mathbb{N}$ denotes a computable map. Even more, proof assistants are very good at computing with them, so it remains questionable what the advantage of CR would be (other than extracting maps from totoal relations, which is a form of choice).

@AndrejBauer yeah I figured it was a bit extravagant (but perhaps there was a tiny proof-of-concept proof assistant that implemented it?). A use case I had in mind: if you have or are in the process of formalizing computability theory in the proof assistant, CR is a convenient way to prove a function of computable, so having it as a built-in tactic is convenient. The requirement that the proof assistant actually produces $e$ is just a preference for the proof assistant being able to compute things (just adding an axiom is obviously easy).

You should ask a separate question: how to formalize computability theory? The answer is very nice and cannot be done justice in a comment.