I've wondered how a type theory/proof assistant could manage to add countable choice (or its dependent choice version) as something primitive as well as to keep the computational properties, e.g., canonicity.
The axiom of countable choice is important in analysis that it allows real numbers behaving much familiar for classical-minded mathematicians. It is thought by some people "constructive" since it can be justified in effective topos. Also, it holds in many type theories as meta-theorem, at least in the empty context. However, it seems mainstream proof assistants do not incorporate it into their core languages. So I was wondering if anyone has ever figured out how to do that?
This question is related to What axioms have a computational interpretation? and Incorporating Markov's principle in various proof assistants.
P.S. Choice is subtle in type theory admittedly, so maybe I should add that we understand the axiom of choice as so-called Extensional Axiom of Choice or the propositional-truncated version in HoTT (c.f. HoTT Book Chapter 3.8), instead of the form "trivially true in constructive type theory" which has no essential logical consequence.
P.P.S. Other forms of choice are also welcomed!
P.P.P.S. I prefer answers about "computationally sensible type theory which validates countable choice" as elaborated shortly in Andrej Bauer's answer. I think cubical type theory is a perfect example that a new type Glue is introduced with full reduction rules so that axiom of univalence can be proved and computed. I want to know if similar things can be done for countable choice.