Coq: defining a function based on uniqueness and existence theorems

Question

To isolate this issue as much as possible, suppose I begin a Coq session as follows.

Parameter A : Type.
Parameter B : Type.
Parameter P : A -> B -> Prop.

Axiom existence : forall a : A, exists b : B, P a b.
Axiom uniqueness : forall a : A, forall b b' : B, P a b -> P a b' -> b = b'.

From here, I want to define a function f : A -> B as the unique function for which P a (f a) is always true.

How can I do this? Can I do this? Obviously I ought to begin with something like

Definition f : A -> B.
  intro a.
  assert (E := existence a).
  assert (U := uniqueness a).

...but how do I actually write the function in terms of these hypotheses?

Answer 1

I believe it is not possible in your current setting.

The problem is that you can extract the b from your existence theorem, but this can only live in Prop.

So, I believe you either have to move A and B in Prop, or to move existence and uniqueness in Set.

This would result in either of these:

---

Parameter A : Prop.
Parameter B : Prop.
Parameter P : A -> B -> Prop.

Axiom existence : forall a : A, exists b : B, P a b.
Axiom uniqueness : forall a : A, forall b b' : B, P a b -> P a b' -> b = b'.

Definition f : A -> B.
  intro a. destruct (existence a) as [b _]. exact b.
Defined.

---

Parameter A : Set.
Parameter B : Set.
Parameter P : A -> B -> Prop.

Axiom existence : forall a : A, { b : B | P a b }.
Axiom uniqueness : forall a : A, forall b b' : B, P a b -> P a b' -> b = b'.

Definition f : A -> B.
  intro a. destruct (existence a) as [b _]. exact b.
Defined.

---

It is quite possible that neither of these is actually what you want. In that case, I would need more details to be able to help. It might be that you're willing to do something that is not possible in an intuitionistic setting.

PS: I am no expert.