The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

I am dissatisfied with the form of the axiom of dependent description,
as it is given in Logic/ClassicalDescription.v and the associated
theorems.

Axiom
  dependent_description :
    forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
      (forall x:A,
          exists y : B x, R x y /\ (forall y':B x, R x y' -> y = y')) ->
       exists f : forall x:A, B x, (forall x:A, R x (f x)).


This axioms gives me the existence of a function but not the possibility
to use this function easily in further definitions.  I believe a
stronger version would be the following one:

Axiom
  dependent_description' :
    forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
      (forall x:A,
          exists y : B x, R x y /\ (forall y':B x, R x y' -> y = y')) ->
       sigT (fun f : forall x:A, B x => (forall x:A, R x (f x))).

(the difference between dependent_description and dependent_description'
is that I replaced the last exists by sigT. )

I would like to know whether adding this axiom would yield an
inconsistent logic.  Morally, I would be satisfied with the idea that,
in classical logic, the functional notation of Coq is just a short-hand
for "set-theory-like" functions but I am aware that we may be navigating
close to Cantor's naive set theory 

I believe the answer can fall in three categories:

1/ No problem, you can already derive dependent_description' from
   dependent_description using other axioms of classical logic that
   are thought to be sensible (a coq proof would be great).

2/ Big problem, once you do that, you can encode one of the well-known
   paradoxes (again a coq proof would be great).

3/ Nobody knows.

Does anyone have a quick answer in the direction of 1 or 2?  Does anyone
know that we don't know?

Yves