[ draft ] Refactor Dec to use constructive negation

[gallais]

Now that v3.0 is being worked on, I think it is the
right time for me to push us to rethink our approach
to Dec.

Historically Dec was just a datatype with yes/no
constructors choosing between A and ¬ A.

In #929 we entered the era of Reflects and the idea
that we could separately compute the Bool telling
us the outcome of the decision procedure from the
actual proof that comes from its correctness.

In this draft, I'd like to shed the commitment to ¬_
in favour of a solution offering constructive notions
of negation.

This is based on @bobatkey's work:

• https://bentnib.org/posts/2023-01-15-datatypes-with-negation.html
• https://bentnib.org/posts/2023-11-02-more-data-types-with-negation.html

and @jfdm has been porting some of these ideas to Idris.

I am opening this PR so that we can discuss the design
before I push my experiment further.

---

The core of the design behind this specific incarnation is
that we start by describing what it means for two types
to be orthogonal with respect to a (vocabulary influenced by
realisability) "pole" P. We say these types are P-orthogonal.

A type is always P-orthogonal to its literal negation but
there may be more constructive notions of negation e.g.
_≤_ is orthogonal to _>_, (A × B) is orthogonal to (¬A ⊎ ¬B),
or even (¬A ⊎ (A × ¬B)) if we record the left-biased nature
of the decision procedure in the type.

The pole idea gives us the ability to decide how strict the
orthogonality should be. ⊥-orthogonality is the usual "not
both at the same time" whereas ⊤-orthogonality is always
trivially true of any pair of types.

The orthogonality combinators allow us to build a type of
constructive orthogonals to types built out of the standard
type constructors.

Once we have our orthogonal types, we introduce Choice as
the generalisation of Reflects. Choice is a Boolean-indexed
decision between two orthogonal types.

This covers:

1. the usual strong decidability Dec by having a choice
   between a type and its negation

2. a variant with constructive negation by simply demanding
   two ⊥-orthogonal types

3. weak decidability by letting the pole be ⊤ and writing
   a choice function between A and ⊤

[jamesmckinna]

Interesting!
(But... 'Pole' ideas surely predate Bob, going back to Girard/Krivine, at least? I confess I'm not across all the details, so back to the school books!)

Let me rephrase the above in slightly less judgmental/prejudicial terms:

• what's the relationship between Atkey-style, and Girard/Krivine-style?
• what's the relationship between Altkey-style and minimal logic wrt P, defining ¬ A = A -> P and reasoning under assumptions governing P?
• does Altkey-style admit similar kinds of results to those in proof theory/realisability, such a Friedman A-translation, and conservativity of PA over HA for PI^0_2 statements... etc.?
• ...

[jamesmckinna]

On matters of 'syntax'/'representation', please also see #2058 / #2155 and consider deprecating ofʸ/ofⁿ, possibly even in terms of of as a constructor, with the old names as pattern synonyms?

[Taneb]

Are there any other values that might get used as the pole in interesting situations?

[shhyou]

A typed reduction relation and the progress lemma, perhaps?

[gallais]

consider deprecating ofʸ/ofⁿ, possibly even in terms of of as a constructor

Unfortunately both branches of an if_then_else_ need to live in the same universe
so of is strictly less expressive than the ofʸ/ofⁿ pair.