The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi Yves,

  Benjamin essentially said what I planned to say. 

  Indeed, as a side-product of Chicli-Pottier-Simpson's paradox [1],
all what you can prove with the version prime (yielding a Sigma-type
in Type), you can already prove it with the version in Prop, _as soon
as you ultimately prove a proposition_ (*).  Hence, you don't have
more proofs of a paradox with the version in Type than with the
version in Prop. [Incidentally, both are inconsistent in presence of
classical logic and impredicative Set.]

  Extensionality is not needed (I attach a proof which is basically
Benjamin's proof with unicity hard-wired in Benjamin's "cdom").

  On the practical side: an interest in the description principle is
precisely to be able to declare functions without to specify in
advance the propositional contexts in which they will be used. Hence,
the version in Type actually corresponds more to what we expect. Of
course, this breaks extraction, since the axiom computationally
specifies an oracle.

  So, if nobody objects, I suggest we move dependent_description to
Type for the next release of Coq.

  By the way, notice that description in Type + excluded-middle in
Prop implies excluded-middle in Type. Thinking set-theoretically (what
is generally admitted sound in the absence of Set-impredicativity),
this is indeed no problem.

  Hugo

[1] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical
    Quotients and Quotient Types in Coq, Proceedings of TYPES 2002,
    Lecture Notes in Computer Science 2646, Springer Verlag.

(*) You need some work to show that any use of version prime on some
parameter in a term not of type Prop that is a subterm under some
local context of a term of type Prop, can be simulated by applying the
version in Prop at the upper Prop level, on a parameter generalised
over its local context (this is I think the essence of Benjamin's
proof). Marginally, you also need to ensure that any inductive
definition that relies on the witnesss provided by version prime can
be declared in advance, possibly using a generalisation of it.
Notation "'exists' ! x : A , P" := 
  (exists x : A,  (fun x => P) x /\ forall x':A, (fun x => P) x' -> x = x')
  (at level 200, x ident, right associativity) : type_scope.

Definition 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) ->
       exists f : (forall x:A, B x), forall x:A, R x (f x).

Definition 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) ->
       sigT (fun f : forall x:A, B x => (forall x:A, R x (f x))).

Theorem relative_consistency : 
  (dependent_description' -> False) -> (dependent_description -> False).
Proof.
intros H DepDescr.
pose (A0 := sigT (fun (A:Type) => 
            sigT (fun (B:A->Type) =>
            sigT (fun (R:forall x:A, B x -> Prop) =>
            sigT (fun (p:(forall x:A, exists ! y : B x, R x y)) => A))))).
pose (x0 := fun x:A0 => projT2 (projT2 (projT2 (projT2 x)))).
pose (B0 := fun x:A0 => projT1 (projT2 x) (x0 x)).
pose (R0 := fun x:A0 => fun y:B0 x => projT1 (projT2 (projT2 x)) (x0 x) y).
pose (H0 := fun x:A0 => projT1 (projT2 (projT2 (projT2 x))) (x0 x)).
destruct (DepDescr A0 B0 R0 H0) as (f, Hf).
apply H.
intros A B R H'.
pose (f' := fun x:A => 
           f (existT (fun _ => sigT _) A 
             (existT (fun _ => sigT _) B 
             (existT (fun _ => sigT _) R
             (existT (fun _ => A) H' x))))).
pose (Hf' := fun x:A => 
          Hf (existT (fun _ => sigT _) A 
             (existT (fun _ => sigT _) B 
             (existT (fun _ => sigT _) R
             (existT (fun _ => A) H' x))))).
exists f'.
exact Hf'.
Qed.