Library Coq.Logic.ClassicalDescription
This file provides classical logic and definite description, which is
equivalent to providing classical logic and Church's iota operator
Classical logic and definite descriptions implies excluded-middle
in Set and leads to a classical world populated with non
computable functions. It conflicts with the impredicativity of
Set
The idea for the following proof comes from ChicliPottierSimpson02
Church's iota operator
Axiom of unique "choice" (functional reification of functional relations)
Theorem 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)).
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)).
Compatibility lemmas