Agda-stdlib: Add `Axiom.*` modules for common axioms

[gallais]

It would be nice to have the axioms people typically use to extend
Agda's theory available directly in the standard library. We can also
have result about e.g. their inter-derivability.

See for instance Coq's Logic modules https://coq.inria.fr/distrib/current/stdlib/
for inspiration.

Here is a tentative list:

• [x] Excluded middle (informative & irrelevant?)
• [x] Functional Extensionality (for implicit functions too!)
• [ ] Hilbert's Epsilon
• [x] UIP

[andreasabel]

I suggested something along these lines to Nisse a couple of years ago. Now we can get it!

[MatthewDaggitt]

I'll leave this to you @gallais as I'm definitely shaky on Agda's theory!

[MatthewDaggitt]

There's a little bit of stuff in Relation.Nullary.Negation about excluded middle and double negation elimination. It'd be fine to move it out to the new modules though.

[alhassy]

How would one go about doing this? Surely the usage of postulate's is out of the question. Do we then go for modules paramterised by such axioms?

[gallais]

I would give a type corresponding to the axiom and then the user is free to postulate
it if they want. The results can indeed be defined in a parameterised module.

Something like this (absurd example, of course):

module Axiom.Empty where

Empty : Set
Empty = ⊥

module _ (prf : Empty) where

  anything-goes : {a : Level} {A : Set a} → A
  anything-goes with prf
  ... | ()

Of course if the axiom is level polymorphic then it will not fit in a simple Set l so you
should have something like

module Axiom.Pointed where

AllInhabited : {a : Level} → Set a → Set a
AllInhabited A = A

module _ (pr : ∀ {a} (A : set a) → AllInabited A) where
  (...)

It may be worth naming these modules I have left anonymous. This way if the user
decides to postulate the axiom they can open it applied.

[gallais]

We now have some UIP results in Relation.Binary.PropositionalEquality which should
probably be extracted to (and documented in) Axiom.UIP at some point.

[MatthewDaggitt]

Hmm if you think that's where they belong, probably better to move them now before v1.0?

[MatthewDaggitt]

I'm going to mark this is closed as we've got the axiom structure sorted. If someone needs Hilbert's epsilon in particular shouldn't be difficult to add it in!