The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

It's a reformulation of functional choice (as defined in 
https://coq.inria.fr/library/Coq.Logic.ChoiceFacts.html#FunctionalChoice), 
proof in attached file.

Gaëtan Gilbert

On 28/04/2017 23:17, John Wiegley wrote:
> Is there any way to prove the following, or reduce it to a consistent axiom?
>
>    Theorem inhabited_forall :
>      ∀ A (P : A -> Type), (∀ x, inhabited (P x)) -> inhabited (∀ x, P x).

Require Import ChoiceFacts Utf8.

Definition inhabited_forall :=
    ∀ A (P : A -> Type), (∀ x, inhabited (P x)) -> inhabited (∀ x, P x).

Lemma choice_to_inhab : DependentFunctionalChoice -> inhabited_forall.
Proof.
intros choose.
intros A P HP.
assert (HP' : forall x, exists y : P x, True).
{ intros x;destruct (HP x) as [Hx];exists Hx;trivial. }
pose proof (choose _ _ _ HP') as [f _].
constructor;exact f.
Qed.

Lemma inhab_to_choice : inhabited_forall -> DependentFunctionalChoice.
Proof.
intros choose.
apply non_dep_dep_functional_choice. intros A B R H.
assert (H' : forall x, inhabited {y : B | R x y}).
{ intros x;destruct (H x) as [y Hx];constructor;exists y;exact Hx. }
apply choose in H'. destruct H' as [f].
exists (fun x => proj1_sig (f x)).
intros x;apply proj2_sig.
Qed.