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 is an element of . An element of consists of a real number and a positive integer , such that , because an element of is not presented until both and are given. One and the same real number can be associated with two distinct (but equal) elements of . Nevertheless we shall continue to refer loosely to a positive real number . On those occasions when we need to refer to an for which , we shall take the position that it was there implicitly all along.

In other words, the proposition really stands for the type
of all with . Bishop does not appear to be aware of the
propositions-as-types interpretation in this book, but he uses it implicitly.