Adds `Relation.Nullary.Recomputable` plus consequences

[jamesmckinna]

Fixes #2199 , and the Recomputable and Irrelevant instances of #2091 . Cherry-picks some of the lower-hanging fruit from #2149 .

Outstanding issues:

• [x] names of things: recompute vs. recomputable vs. ...⇒recomputable in all the various places; also the various additions to Relation.Nullary.Negation.Core; UPDATED sticking with recompute for now
• [x] deprecations: module Data.Empty.Irrelevant could now be deprecated entirely, but I have not (yet) done so; similarly, there may be knock-on deprecations arising from name choices above; UPDATED no deprecations!
• [x] where things should live/be (re-)exported from. UPDATED see @JacquesCarette 's comments and my revised commits

(Definite~~Probab~~ly) Won't do in relation to issues raised as a result of #2199 :

• "induction on the negative fragment": a separate (relativised!) Data.Universe construction for the 'Harrop' universe, as Relation.Nullary.Recomputable.Universe, with a view to generalising Harrop's results to ones of the form "if everything in 𝕌 = (U, El) is Recomputable/Irrelevant/Decidable... then so too is everything in Harrop 𝕌 etc. (UPDATED: downstream PR, but only once I've figured it out)
• relationship with the 'Irrelevance Axiom' or @nad 's developments mentioned there. (Ditto.)

[jamesmckinna]

Converting to DRAFT for the time being as I haven't had the brain space to revisit the questions above. UPDATED: punting those downstream!

[jamesmckinna]

Incoming commits tidy this up, and then ready for review. Leaving the 'hard' questions for downstream development.

[jamesmckinna]

I further conjecture on #2329 that all uses of ⊥-elim can be replaced by their irrelevant version ⊥-elim-irr... so question for the maintainers, are we prepared to embrace such a (breaking?) change to the type of ⊥-elim?

[MatthewDaggitt]

so question for the maintainers, are we prepared to embrace such a (breaking?) change to the type of ⊥-elim?

Yes, but in v3.0! I suggest we make an issue with the 3.0 milestone?

[jamesmckinna]

@MatthewDaggitt fair point, but my belief (Modulo the merge conflict) is that everything here is v2.1 compatible so I won't pursue further changes this time around... ;-) And indeed I've now reverted the last round of changes (I think otherwise harmless, but glaring, which invoked weak-contradiction throughout... it's a terrible name, so I welcome a review which offers a better one!)

[jamesmckinna]

@JacquesCarette after the merge of #2329 could you review this one please?

[jamesmckinna]

Now : proofs computed using recompute are irrelevant, so UIP follows immediately from DecidableEquality. I've added these in as further low-hanging-fruit cherry-picked from #2149 UPDATED: but this construction (recomputable implies constant) should be pulled back as far as Recomputable itself... Now DONE. That's it!

[jamesmckinna]

@MatthewDaggitt are you happy with this not being a breaking change now?

[jamesmckinna]

As I understand things, there are (now!) two outstanding issues:

• is this PR breaking or not? I claim it is not, because specifically: in the top-level stdlib API, the public export of recompute (and now, additionally, recompute-constant}) from Relation.Nullary is still that from Relation.Nullary.Decidable (and hence from Relation.Nullary.Decidable.Core), and not that of the newly introduced Relation.Nullary.Reflects.recompute{-constant}.
• does https://github.com/agda/agda/issues/7193 affect the 'safety' of this PR? From my (limited) understanding of @dolio 's reply to my question there, the answer is also that it does not.

Hope this helps! (And removes any further obstruction to merging...)

[JacquesCarette]

Just need @gallais to re-review.

[jamesmckinna]

Just need ... to re-review.

And @MatthewDaggitt ?