names of things (vol. 94): Relation.Nullary.Reflects

[jamesmckinna]

In the course of #2055 (which has grown quite a bit, albeit in essentially trivial ways), I kept banging my head against Reflects.invert, and its friend of.

I'm loath to change already-chosen constructor names (though personally find ofʸ and ofⁿ annoying: why not ofᵗ and ofᶠ which at least correlate typography with semantics?), as they can be worked around with pattern synonyms, but functions are harder, requiring renaming/deprecation... (boo-hoo).

I don't find of at all helpful, even though it is, at least, derived from the above constructors. I find invert even worse, as it's not at all obvious what is even being inverted; in that respect, at a pinch, of⁻¹ might already be a better name.

But 'really', both these operations are the introduction and elimination forms of the Reflects view (there's a separate issue about it being called an 'idiom' in the stdlib, when from my perspective, it simply is a Set-indexed view of Bool), so custom and practice elsewhere in the library suggests the following renaming/deprecation:

• of ↦ reflects⁺
• invert ↦ reflects⁻

Yes? No! Maybe!? (See also #2155 for an alternative naming scheme)

Similarly, rather than the heavy and verbose toWitnessTrue etc., and going with the grain of Yes/No (types of values of answers to questions) instead of True, False (judgments of fact, much weightier epistemologically, cued by the scare quotes around "truth" in the comments), suggest instead for Relation.Nullary.Decidable.Core:

• True ↦ Yes
• False ↦ No
• toWitness ↦ yes⁻
• fromWitness ↦ yes⁺
• toWitnessFalse ↦ no⁻
• fromWitness ↦ no⁺
  etc. for From-yes... etc.