(*|
一意選択公理
============

Definite descriptionという公理から一意選択公理が成り立つことを示す。
|*)

From Stdlib Require Import Logic.Description.

Check constructive_definite_description. (* .unfold *)

(*|
Definite descriptionは一意存在の証明からその項を取り出すことができる。上記の ``A : Type`` は暗黙の引数である。
|*)

Section UniqueChoice.
  Variable A B : Type.

  Definition functional_definite_description :
    forall R : A -> B -> Prop,
    (forall x : A, exists! y : B, R x y)
    -> { f : A -> B | forall x : A, R x (f x)}.
  Proof.
    intros.
    set (F :=
      fun a => constructive_definite_description (R a) (H a)
    ).
    exists (fun a => proj1_sig (F a)).
    intro a.
    exact (proj2_sig (F a)).
  Defined.

  Theorem unique_choice :
    forall R : A -> B -> Prop,
    (forall x : A, exists! y : B, R x y)
    -> exists f : A -> B, forall x : A, R x (f x).
  Proof.
    intros.
    apply ex_of_sig.
    apply functional_definite_description.
    assumption.
  Qed.
End UniqueChoice.