# Indefinite description axiom could be simpler?

Putting this in “Miscellaneous” for now because while it feels a bit like a proposal, it is really not important enough to make one formally; I’m just curious about the design consderations of the standard library.

The axiom `constructive_indefinite_description`, as postulated in `Coq.Logic.IndefiniteDescription`, has the following type:

``````Definition indefinite_description :=
forall (A : Type) (P : A->Prop), ex P -> sig P.
``````

This is straightforward enough, but I cannot help but compare it to another possible axiom which is even simpler in concept:

``````Definition simple_description :=
forall (A : Type), inhabited A -> A.
``````

These two are provably equivalent:

``````Proposition simple_description_implies_indefinite_description :
simple_description -> indefinite_description.
Proof.
intro d. repeat intro.
apply d; firstorder.
Defined.

Proposition indefinite_description_implies_simple_description :
indefinite_description -> simple_description.
Proof.
intro d. repeat intro.
apply proj1_sig with (P := λ _, True), d; firstorder.
Defined.
``````

Why is the former proposition, rather than the latter, the one given as an axiom in the standard library? It doesn’t really matter (that’s the whole point of being equivalent) but I find the latter just more aesthetic somehow in its directness, and it seems to be somewhat clearer (and more honest perhaps?) with regard to what the axiom ‘does’.

Indeed, your version is conceptually purer. That would be worth to rephrase the file `IndefiniteDescription.v` from the `inhabited A -> A` variant. If you feel so, you could propose a pull request.

For consistency’s sake, could we also rephrase `Logic.ClassicalEpsilon.v` the same way ?
Or make `ClassicalEpsilon.v` require `IndefiniteDescription` ?

Requiring `IndefiniteDescription.v` in `ClassicalEpsilon.v` would indeed be a simple thing to do.

The constants `epsilon` and `iota` are defined in both files `Epsilon.v` and `ClassicalEpsilon.v`. Would it be useful to share as much as possible the axioms and definitions of both files ?
If so, I may have a look at the beginng of September.

Would it be useful to share as much as possible the axioms and definitions of both files ?

`ClassicalEpsilon.v` can include `IndefiniteDescription.v` but the
file `Epsilon.v` makes otherwise assumptions a priori weaker than the assumptions in `ClassicalEpsilon.v` (something like a form of independence of premisses vs full classical logic), so I don’t know how much could be shared. Both have different motivations.

huh confused about definite description here

I guess you would want

``````Definition unique A := forall (x y: A), x = y.

Axiom definite: forall A, inhabited A -> unique A -> A.
``````

So I was going to say this doesn’t work well for extending to definite description but it might have a nice univalent interpretation. `unique` is hProp.