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.