How do real numbers like Pi, golden ratio, etc fit into type theory
If by &quot;non-terminating real number&quot; you mean to say that the digit expansion of the number is an infinite sequence, then that is not saying much, because every real number is &quot;non-terminating&quot; in this sense, even the real number 42, for its digit expansion is
$$41.999999999999999999999999999999....$$
In any case, nobody suggests that the digits must somehow be computed all at once, although that is a common misconception that arises in the study of computability of reals. We just need a method which computes any digit we desire – but we never desire all the digits at once.
A sequence of digits is a function $f : \mathbb{N} \to \mathbb{N}$, and such functions can be perfectly managed by type theory. In fact, the correct way to represent a real number by a sequence is to use positive and negative digits, or else you can't compute certain operations (such as $+$). So in reality, in type theory or in any other setting a real number may be represented by a sequence of digits $f : \mathbb{N} \to \{-9, -8, \ldots, 8, 9\}$. Even better but equivalent is the representation by which a real number is represented by a map $g : \mathbb{N} \to \mathbb{Q}$ satisfying the condition $\forall m, n \in \mathbb{N} \,.\, |g(m) - g(n)| &lt; 2^{-\min(m,n)-1}$. Such a map represents the number $\lim_n g(n)$.
All of the above can be stated in type theory:
$$
\Sigma (g : \mathbb{N} \to \mathbb{Q}) \,
\Pi (m, n : \mathbb{N}) \;
\mathrm{Id}_\mathbb{Q}(1, \max(|g(m) - g(n)| \cdot 2^{1 + \min(m, n)}, 1))
$$
The inner $\mathrm{Id}$-type says
$$\max(|g(m) - g(n)| \cdot 2^{1 + \min(m, n)}, 1) = 1$$
which is just a fancy way of stating
$$|g(m) - g(n)| \cdot 2^{1 + \min(m, n)} \leq 1.$$