A pillow’s softness, from how it behaves:

To forces it reacts yet it conforms.

The patient repitition of a wave,

Transforming an atom from form to form.

How everything existing had begun,

Matter from matter moving fast away.

How everything is hidden in the sum

Of amplitudes of all the different ways.

Yet all the things I do ’till now express

Are mere fragments of a deeper core.

How would I love to faithfully address

The full wonders with all of their galore.

Yet when I try those feelings to compose

My poetry is hightened into prose.

# Monthly Archives: January 2013

# 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

isan element of . An element of consists of a real numberanda 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.