# Propositions as types in Foundations to Constructive Analysis

I was reading Foundations of Constructive Analysis by Errett Bishop, and I came across this intersting passage:

It is not strictly correct to say that a real number $\{x_n\}$ is an element of $\mathbf{R}^+$. An element of $\mathbf{R}^+$ consists of a real number $\{x_n\}$ and a positive integer $n$, such that $x_n > n^{-1}$, because an element of $\mathbf{R}^+$ is not presented until both $\{x_n\}$ and $n$ are given. One and the same real number $\{x_n\}$ can be associated with two distinct (but equal) elements of $\mathbf{R}^+$. Nevertheless we shall continue to refer loosely to a positive real number $\{x_n\}$. On those occasions when we need to refer to an $n$ for which $x_n > n^{-1}$, we shall take the position that it was there implicitly all along.

In other words, the proposition $x \in \mathbf{R}^+$ really stands for the type
of all $n$ with $x_n > n^{-1}$. Bishop does not appear to be aware of the
propositions-as-types interpretation in this book, but he uses it implicitly.