The Coq mailing list

[Benjamin Werner <werner>]

     Salut David,

The set-theoretic axiom of choice has indeed some non-trivial
interactions with type theory. In the case you consider, I think
however there should be no foundational problem with the axiom. 

Checking it with full accuracy would take a little work since:

1) You place yourself at a quite high-level. That is you consider the
set-theoretic axiom of choice, in Gilles Kahn's version of sets, and
not a more basic type-theoretic version of the axiom. In other words,
this is a quite verbose version of AC.

2) You certainly work in a context in which you allready have assumed
other axioms. But again, my strong guess is that your various axiom
should coexist in the simple set-theoretic model for Type and Prop.


A more basic version of the choice axiom is what I use in the full
encoding of ZFC set theory (contrib Rocq/ZF)(*). That is:

Definition EquivRel := [A:Type][R:A->A->Prop]
  ((x:A)(R x x)
 /\(x,y:A)(R x y)->(R y x)
 /\(x,y,z:A)(R x y)->(R y z)->(R x z)).

Definition Tchoice := (A:Type)(R:A->A->Prop)(EquivRel A R)->
  (EX ? [f:A->A](((x:A)(R x (f x)))
               /\((x,y:A)(R x y)->(f x)==(f y)))).


(where EX is an existential over Type, living in Prop, you should
probably adapt the syntax).

I suspect this axiom should allow you to prove what you want.


An amusing side-effect is that this axiom is actually sufficient to
prove the excluded middle by a Diaconescu-style construction.



(*) now that I write this, I realize I forgot to add the corresponding
file in the distribution. This will be corrected for the next release
and interested users can ask me for the full version of the encoding
of ZFC in Coq.





Cheers,


Benjamin Werner
----------------------------------------------------------------------------
Projet Coq
INRIA-Rocquencourt, BP 105, F-78 153 LE CHESNAY cedex, FRANCE
E-mail: 
Benjamin.Werner AT inria.fr
Phone:  +33 (1) 39 63 52 31
Mobile: +33 (6) 10 25 46 50
Fax:    +33 (1) 39 63 56 84
http://coq.inria.fr/~werner/
-----------------------------------------------------------------------------