Indefinite description axiom could be simpler?

Miscellaneous
1

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’.

2

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.

3

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

4

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

5

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.

6

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.

7

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.