+(**************************** The axiom of choice *****************************)
+
+(* The axiom of choice says that given a collection of non-empty sets S_i
+indexed over a base set I, it is possible to make a selection of exactly one
+element x_i ∈ S_i.
+In type theory, this can be expressed in the following terms: *)
+
+axiom choice_ax: ∀I:Type[0].∀S:I→Type[0].∀A:(∀i:I.S i → Type[0]).
+ (∀i:I.(∑x:S i.A i x)) → ∑f:∀i:I.S i.∀i:I.A i (f i).
+
+(* The axiom of choice is independent from the traditional basic axioms of set
+theory, like Zermelo–Fraenkel set theory, hence, if required, must be explicitly
+added to the theory. This extension of ZF, known as ZFC, provides the "standard"
+axiomatization of set theory.
+
+The controversial nature of the axiom of choice is related to the effectiveness
+of performing the selection claimed by the axiom of choice; for this reasons the
+axiom of choice is usually rejected by constructive mathematicians.
+
+However, if the proof of the existence on an inhabitant x_i for each type S_i is
+itself constructive, then this proof already provides a method that, when
+applied to an element i∈I returns the witness x_i. In other words, not only the
+above axiom "choice" is perfectly acceptable, but it is actually provable! *)
+
+theorem choice: ∀I:Type[0].∀S:I→Type[0].∀A.
+ (∀i:I.∑x:S i.A i x) → ∑f:∀i:I.S i.∀i:I.A i (f i).
+#I #S #A #H
+(* The goal is
+ ∑f:∀i:I.S i.(∀i:I.A i (f i))
+We need to provide the function f:∀i:I.S i, and the proof that for any i:I,
+A i (f i). The hypothesis H tells us that for any i we can build an object
+(H i): ∑x:S i.A i x. The first projection of (H i) is an element of type (S i),
+and we may define f ≝ λi. DPair_fst … (H i).The second projection of (H i) is
+a witness of A i (DPair_fst … (H i)), that is, according to our defintion
+of f, a witness of A i (f i). Hence, λi.DPair_snd ?? (H i): ∀i:I.A i (f i). *)
+%{(λi.DPair_fst ?? (H i)) (λi.DPair_snd ?? (H i))}
+qed.
+
+(* It is worth to observe that if we try to repeat the same proof with either
+the existential of the sigma type it will not work. For instance, the
+following property is not provable: *)
+
+axiom Pchoice: ∀I:Type[0].∀S:I→Type[0].∀A.
+ (∀i:I.∃x:S i.A i x) → ∃f:∀i:I.S i.∀i:I.A i (f i).
+
+(* The point is that the proof would require to extract from a non-informative
+content, namely the fact that there exists an x such that (A i x), the actual
+witness x, that is an informative notion, and we know that this is forbidden for
+consistency reasons. *)
+
+
+
+