The Coq mailing list

[roconnor AT theorem.ca]

On Wed, 9 Nov 2011, Carlos Simpson wrote:

> I would claim that there is a difference between being sometimes interested in
> types with computational content; and requiring *all* types to have
> computational content. Regarding R and Q: let Q' be the type of 1-element
> subsets of Q, which if we assume proper quotients, can be defined. Then
> we can define non-constant functions R-> Q'. The projection Q->Q' is
> bijective but doesn't admit an inverse, since Q has decidable equality but
> not Q'. Or in another direction, given a quotient
> X/r, you can still look at the setoid (X,r), indeed for some parts of
> the discussion it will undoubtedly be essential to do so.
> Assuming quotient types would just allow you to sometimes consider types
> which aren't setoids.

What you suggest above is fine.  In fact, the tick in Q' is almost the 
same as what I call the classical value monad in my paper, "Classical 
mathematics for a constructive world", except that I use (double negation) 
stable setoids instead of quotients and require the 1-element predicates 
to be stable.  The Kleisli arrows for this classical value monad gives you 
a classical function space which lets you do most of your classical style 
mathematics.  You even get classic definite description for classical (aka 
stable) propositions and hence classic definite choice as a theorem. 
(And furthermore, classical indefinite description is a consistent 
proposition and could be added to a type theory such as OTT without losing 
canonicity of the non-Prop universe.)

I don't immediately see any problems using a proper quotient type here 
instead of a stable setoid.

Using the classical value monad and classical function spaces is IMHO a 
great way for people wanting to do classical mathematics (such as Victor) 
to do so in constructive type theory (after all, constructive mathematics 
is *more* expressive than classical mathematics).  You don't need to 
assume any axioms, so the work is usable for people doing constructive 
mathematics.  As I point out in my paper, there are several examples of 
places in constructive mathematics where we want to use classical results.

But it is important to understand that, of course, you don't get 
constructive functions when you use classical function spaces and they 
won't be usable for computation.

--
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.''