Enhancement to `Relation.Nullary.Reflects` etc.

[jamesmckinna]

This is a minimally invasive extension to Relation.Nullary.{Reflects|Decidable|Decidable.Core} to achieve the following:

• two 'better'/more dependent eliminators for Reflects which streamline various constructions, including invert (now as an alias for reflects⁻¹ against downstream renaming/deprecation cf. #2058 #2155);
• proofs that reflects/reflects⁻¹ form an iso pair of operations;
• Reflects now defines a Nullary property Recomputable, and recompute proves Recompute A for any A satisfying Reflects A b; UPDATED but see also #2199 / #2243 for a possible, possibly better, path to take;
• (BUG) correct reference to README.Design.Decidability in Decidable.Core; UPDATED; now fixed by #2183 ; but need to fix up the load paths after #2184
• Decidable.Core now delegates its proof of recompute to Reflects.recompute, with associated import simplification;
• Decidable.Core also refactors the definition of the pattern synonyms yes and no via lazier versions yesᵖ and noᵖ, reflecting the use of lazier/more anonymous pattern matching on yes no elsewhere in the library; but see also https://github.com/agda/agda/issues/7061 for a better potential solution to tackle this;
• simplified imports for Decidable and throughout;
• characterisation of Decidable A in terms of equivalence with existence of a Boolean b such that A is equivalent to T b, cf. comment on #2189
• extended exports of the new functionality from Relation.Nullary.

No CHANGELOG entry: v2.0 introduces the Reflects refactoring of the Nullary sub-hierarchy, so this is simply a non-breaking enhancement to that functionality. As such, I'd like to argue for it being part of v2.0.

The new behaviour is demonstrated in a (modest) refactoring of Axiom.UniquenessOfIdentityProofs.(see also #2243 for a riff on this: the 'essence' of the Hedberg argument is that recompute gives rise to constant functions...)

This could be merged as-is, but in the spirit of a (revised) version of #2055, much more downstream refactoring is possible, eg to exploit the new lazier constructors/rename the reflects/reflects⁻¹ iso pair, and reconciling the duplication raised by https://github.com/agda/agda-stdlib/pull/2055#discussion_r1300290102. But those can also easily follow in v2.1-tagged PRs.

TODO:

• [ ] CHANGELOG for the various recent additions, depending on when this gets merged;
• [ ] naming issues;
• [ ] thinking about/sorting out the higher-level exports from Reflects, in particular to avoid name clashes/ambiguity;
• [ ] review changes.

But otherwise trying hard to resist the temptation to let the mission creep any further, after #2189 already opened some doors to that... !

[JacquesCarette]

The various refactors nicely show the 'worth' of these changes. No strong feeling regarding 2.0/2.1.

[jamesmckinna]

In fact, there's nothing label:breaking about this PR, nor even (yet) label:deprecation. So I'm happy to punt this to v2.1 if need be.

Breaking changes to follow would/might then be

• either to redefine yes and no to be their lazier versions;
• else, to change them from pattern synonyms to definitions (UPDATED: these have now been added, but without deprecation/removal of anything), as compositions of the lazier constructors with of,

the aim being eventually to encapsulate all uses of the ofⁿ and ofʸ constructors; it strikes me that they have no business being part of the public exports from Relation.Nullary{.Reflects}... with the reflects eliminator being part of that destructor-style abstraction.

But all of that is up for discussion/design downstream.

[MatthewDaggitt]

So I'm happy to punt this to v2.1 if need be.

If that's the case, then let's move it. Plenty of things that do need to be in v2.0.

[jamesmckinna]

Advice (eventually!) welcome on handling the CHANGELOG merge conflicts for v2.1-labelled PRs once we have a new master branch post-v2.0 with an initially blank such set of changes...

[jamesmckinna]

So the only thing I haven't done is to systematically replace (NOT deprecate) invert with of⁻¹ in the changed files, as that can wait for the eventual deprecation PR, and once we have an agreed pair of names for of/of⁻¹...

[jamesmckinna]

Marking this now as blocked-by-issue until I/we figure out the consequences of #2199 ... UPDATED and the subsequent #2243 which cherry-picks some of the lower-hanging fruit from here...

[jamesmckinna]

Quick refresh to keep this up-to-date against any (successful!) merge of #2243 on which this PR is currently blocking.

[jamesmckinna]

Progress on #2243 if successfully merged, will mean that this slims down considerably, but none the worse for that! Some further reconsideration might also be in order eg wrt deprecations...

[jamesmckinna]

Closing this in view of the merge conflicts arising from #2243 , which leaves as content only:

• the new lazier patterns
• the renamings of of and invert via reflects etc.
• possible deprecations

and AFAIAC, those can now wait for ... v2.2 at least, and a fresh PR for each of the above (the lazier patterns for example might be a stretch for v2.x, while the other stuff is largely cosmetic...)