What name should we use for (instances of) `DecidableEquality`?

[jamesmckinna]

(derived from #2842 )
Conventionally, we write _≟_ (indeed, this is the field name of IsDecEquivalence in the Setoid case), even when the underlying Setoid is given by _≡_.

That said, derived forms in such instances (as for example exposed in the course of #2843 ) seem to dither as to whether we write:

• _≟_
• ≡-dec (NB. not infix!)
• _≡?_ which @gallais argues for, persuasively in my view [ fix ] Relation.Nullary.Decidable.Core names for combinators #2843 (comment)
• others, such as the generic combinator name *-decidable eg. [ fix ] Relation.Nullary.Decidable.Core names for combinators #2843 (comment)

This is one of the more pervasive examples, but serves as a prototype for subsequent related design issue/naming choices under #2846 .

We should, if possible, decide, and tidy up the library (and style-guide!) to reflect our agreed choice.

[Taneb]

I'm of the opinion that _≟_ is the correct symbol only when the underlying equivalence is _≡_, noting the straight bars and that we can't have _=_ has an identifier in Agda. There isn't a unicode symbol "questioned approximately equal to" or a "question mark above combining character" though :(

[Taneb]

Thinking about it for thirty seconds longer, I think that that's a good enough reason we shouldn't use _≟_ for this. _≡?_, with the exact symbol changing to match the corresponding relation, would be more clear in almost any use case

[JacquesCarette]

_≡?_ seems principled. We might want to leave _≟_ around as a convenience alias for a while, i.e. longer than the usual deprecation cycle.

[jamesmckinna]

We should also update the style-guide to reflect our conclusion(s)...