Library Stdlib.Logic.ClassicalUniqueChoice
This file provides classical logic and unique choice; this is
weaker than providing iota operator and classical logic as the
definite descriptions provided by the axiom of unique choice can
be used only in a propositional context (especially, they cannot
be used to build functions outside the scope of a theorem proof)
Classical logic and unique choice, as shown in
[ChicliPottierSimpson02], implies the double-negation of
excluded-middle in Set, hence it implies a strongly classical
world. Especially it conflicts with the impredicativity of Set.
[ChicliPottierSimpson02] 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.
From Stdlib Require Export Classical.
Axiom
dependent_unique_choice :
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)).
Unique choice reifies functional relations into functions
Theorem unique_choice :
forall (A B:Type) (R:A -> B -> Prop),
(forall x:A, exists! y : B, R x y) ->
(exists f:A->B, forall x:A, R x (f x)).
The following proof comes from [ChicliPottierSimpson02]