The Coq mailing list

[roconnor AT theorem.ca]

Hi Andrej,

On Thu, 3 Nov 2011, Andrej Bauer wrote:

> If you know how to express the fact that S and T have the same
> supremum without using any quantifiers, please let me know.

Section 6 from my paper "Classical mathematics for a constructive world" 
<http://dx.doi.org/10.1017/S0960129511000132> defines a "classical partial 
value monad" which is designed exactly for this purpose of defining these 
classical functions in constructive type theory.  Of course, the monad 
hides an existential quantifier, but it isn't exposed to the user.  The 
user should be able to write functions with just the standard overhead of 
working with a commutative monad.

The monad is defined for a stable setoid Y as

P Y = { YP : Y --> Prop | (forall y : Y, ~ ~ (YP y) -> YP y) /\
                          (forall y1 y2 : Y, YP y1 -> YP y2 -> y1 == y2) }

And supremum can be given the type supremum :: (Y --> Prop) --> P Y
where --> is notation for a respectful funciton and Prop is the setoid of 
propositions under with logical equivalence.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''