I am not sure whether [Yannick Forster](https://yforster.github.io) is hanging out around here, so allow me to refer you to his PhD thesis and his recent research.

Yannick uses the following setup to carry out synthetic computability theory (see his home page to get a feel for how much computability theory he handles):

* calculus of inductive constructions
* a `Prop` with excluded middle
* a form of Church's thesis "all functions are computable"

At first sight this looks contradictory because Church's thesis and excluded middle together produce a contradiction, as we can diagonalize to produce a non-computable function $f : \mathbb{N} \to \mathbb{N}$:

$$
f(n) =
\begin{cases}
k + 1 & \text{if $n$-th computable function outputs $k$ on input $n$}\\
42 \text{otherwise}
\end{cases}
$$
Now, $f$ is total by excluded middle, hence there is some $m \in \mathbb{N}$ such that $f$ is the $m$-th computable function, but then we get $f(m) = f(m) + 1$.

Actually, the above proof secretly used unique choice. When we write down the definition of $f$ carefully, we notice that we actually gave the graph of $f$:
$$F(n,k) \iff
(\text{$n$-th machine on input $n$ outputs $k$}) \lor
((\text{$n$-th machine on input $n$ diverges}) \land k = 42)
$$

Luckily, unique choice is not validated by the calculus of inductive constructions.