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:

• 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
• 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!
• where things should live/be (re-)exported from. UPDATED see @JacquesCarette 's comments and my revised commits

(DefiniteProbably) 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]

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 Agda always has irrelevant projections agda#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]

After review of the latest stuff: it continues to look good and, this time, does look backwards compatible as well.

[andreasabel]

(Reviewing the irrelevance parts): To me, these look like mainstream uses of irrelevance, not affected by agda/agda#7193

[JacquesCarette]

Just need @gallais to re-review.

[jamesmckinna]

Just need ... to re-review.

And @MatthewDaggitt ?