From 9888e50ce40326ccc5c412da396548cf418bfcb0 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Mon, 22 Jun 2026 13:53:03 +0100
Subject: [PATCH] [ draft ] Refactor Dec to use constructive negation
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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.

---

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 ⊤
---
 src/Relation/Nullary/Choice.agda     | 213 +++++++++++++++++++++++++++
 src/Relation/Nullary/Orthogonal.agda | 128 ++++++++++++++++
 2 files changed, 341 insertions(+)
 create mode 100644 src/Relation/Nullary/Choice.agda
 create mode 100644 src/Relation/Nullary/Orthogonal.agda

diff --git a/src/Relation/Nullary/Choice.agda b/src/Relation/Nullary/Choice.agda
new file mode 100644
index 0000000000..b75aba5f3b
--- /dev/null
+++ b/src/Relation/Nullary/Choice.agda
@@ -0,0 +1,213 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of the `Choice` construct
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Nullary.Choice where
+
+open import Agda.Builtin.Equality
+
+open import Data.Bool.Base using (Bool; T; true; false; not; if_then_else_; _∧_)
+
+open import Data.Empty using (⊥; ⊥-elim-irr)
+open import Data.Empty.Polymorphic using () renaming (⊥ to ⊥ˡ)
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
+open import Data.Unit.Base using (⊤)
+open import Data.Unit.Polymorphic.Base using () renaming (⊤ to ⊤ˡ)
+
+open import Level using (Level; _⊔_)
+
+open import Function.Base using (_$_; _∘′_; _∘_; const; id)
+
+open import Relation.Nullary.Negation.Core
+  using (¬_; contraposition; contradiction-irr; contradiction; _¬-⊎_; ¬¬-η)
+open import Relation.Nullary.Recomputable as Recomputable using (Recomputable)
+
+
+open import Relation.Nullary.Orthogonal
+  using (_⫫[_]_; negation; orthogonal; ∁; _∩_; _!∩_)
+
+private
+  variable
+    ℓa ℓaⁿ ℓb ℓbⁿ p : Level
+    A : Set ℓa
+    ¬A : Set ℓaⁿ
+    B : Set ℓb
+    ¬B : Set ℓbⁿ
+    P : Set p
+    oA : A ⫫[ P ] ¬A
+    oB : B ⫫[ P ] ¬B
+    a b : Bool
+
+------------------------------------------------------------------------
+-- `Choice` idiom.
+
+-- The choice between A and B is reflected by a boolean value.
+-- `Choice A B b` is equivalent to `if b then A else B`.
+-- `Choice A (¬ A) b` is equivalent to `Reflects A b`
+
+data Choice
+  (A : Set ℓa) (P : Set p) (B : Set ℓb)
+  (oA : A ⫫[ P ] B) : Bool → Set (ℓa ⊔ p ⊔ ℓb) where
+  ofʸ : (a : A) → Choice A P B oA true
+  ofⁿ : (a : B) → Choice A P B oA false
+
+Reflects : Set ℓa → Bool → Set ℓa
+Reflects A = Choice A ⊥ (¬ A) (negation A)
+
+------------------------------------------------------------------------
+-- Constructors and destructors
+
+-- These lemmas are intended to be used mostly when `b` is a value, so
+-- that the `if` expressions have already been evaluated away.
+-- In this case, `of` works like the relevant constructor (`ofⁿ` or
+-- `ofʸ`), and `invert` strips off the constructor to just give either
+-- the proof of `A` or the proof of `B`.
+
+of : ∀ {b} → if b then A else B → Choice A P B oA b
+of {b = true } a = ofʸ a
+of {b = false} b = ofⁿ b
+
+invert : ∀ {b} → Choice A P B oA b → if b then A else B
+invert (ofʸ a) = a
+invert (ofⁿ b) = b
+
+------------------------------------------------------------------------
+-- Transformation
+
+map : (A → B) → (¬A → ¬B) →
+      Choice A P ¬A oA b → Choice B P ¬B oB b
+map f g (ofʸ a) = ofʸ (f a)
+map f g (ofⁿ b) = ofⁿ (g b)
+
+map₁ : (A → B) → Choice A P ¬A oA b → Choice B P ¬A oB b
+map₁ f = map f id
+
+map₂ : (¬A → ¬B) → Choice A P ¬A oA b → Choice A P ¬B oB b
+map₂ = map id
+
+------------------------------------------------------------------------
+-- recompute
+
+-- Given an irrelevant proof of a reflected type, a proof can
+-- be recomputed and subsequently used in relevant contexts.
+
+recompute : ∀ {b} → Choice A ⊥ B oA b → Recomputable A
+recompute (ofʸ  a) _ = a
+recompute {oA = oA} (ofⁿ b) a = ⊥-elim-irr (oA .orthogonal a b)
+
+recompute-constant : ∀ {b} (r : Choice A ⊥ B oA b) (p q : A) →
+                     recompute r p ≡ recompute r q
+recompute-constant = Recomputable.recompute-constant ∘ recompute
+
+------------------------------------------------------------------------
+-- Interaction with true, false, negation, product, sums etc.
+
+⊥ˡ-choice : Choice A P (¬ ⊥ˡ) oA false
+⊥ˡ-choice = ofⁿ λ ()
+
+⊥ˡ-reflects : Reflects (⊥ˡ {ℓa}) false
+⊥ˡ-reflects = ⊥ˡ-choice
+
+⊤ˡ-choice : Choice ⊤ˡ P B oA true
+⊤ˡ-choice = ofʸ _
+
+⊤ˡ-reflects : Reflects (⊤ˡ {ℓa}) true
+⊤ˡ-reflects = ⊤ˡ-choice
+
+⊥-choice : Choice A P (¬ ⊥) oA false
+⊥-choice = ofⁿ λ ()
+
+⊥-reflects : Reflects ⊥ false
+⊥-reflects = ⊥-choice
+
+⊤-choice : Choice ⊤ P B oA true
+⊤-choice = ofʸ _
+
+⊤-reflects : Reflects ⊤ true
+⊤-reflects = ⊤-choice
+
+∁-choice : ∀ {b} → Choice A P B oA b → Choice B P A (∁ oA) (not b)
+∁-choice (ofʸ a) = ofⁿ a
+∁-choice (ofⁿ b) = ofʸ b
+
+¬-reflects : ∀ {b} → Reflects A b → Reflects (¬ A) (not b)
+¬-reflects = map id ¬¬-η ∘′ ∁-choice
+
+Truth-choice : ∀ b {oA} → Choice (T b) P (T (not b)) oA b
+Truth-choice true  = ⊤-choice
+Truth-choice false = ∁-choice ⊤-choice
+
+-- This could also be implemented using map over Truth-choice
+-- if only we had a conveniently accessible proof of
+-- T (not b) → ¬ T b
+T-reflects : ∀ b → Reflects (T b) b
+T-reflects true  = ⊤-choice
+T-reflects false = ⊥-choice
+
+infixr 2 _×-choice_ _!×-choice_
+
+_×-choice_ : Choice A P ¬A oA a → Choice B P ¬B oB b →
+             Choice (A × B) P (¬A ⊎ ¬B) (oA ∩ oB) (a ∧ b)
+ofʸ  a ×-choice ofʸ  b = ofʸ (a , b)
+ofʸ  a ×-choice ofⁿ ¬b = ofⁿ (inj₂ ¬b)
+ofⁿ ¬a ×-choice _      = ofⁿ (inj₁ ¬a)
+
+_×-reflects_ : Reflects A a → Reflects B b → Reflects (A × B) (a ∧ b)
+ra ×-reflects rb = map₂
+  [ contraposition proj₁
+  , contraposition proj₂
+  ]′ (ra ×-choice rb)
+
+_!×-choice_ : Choice A P ¬A oA a → Choice B P ¬B oB b →
+              Choice (A × B) P (¬A ⊎ (A × ¬B)) (oA !∩ oB) (a ∧ b)
+ofʸ  a !×-choice ofʸ  b = ofʸ (a , b)
+ofʸ  a !×-choice ofⁿ ¬b = ofⁿ (inj₂ (a , ¬b))
+ofⁿ ¬a !×-choice _      = ofⁿ (inj₁ ¬a)
+
+
+{-
+infixr 1 _⊎-choice_
+infixr 2 _×-choice_ _→-choice_
+
+_×-choice_ : ∀ {a b} → Choice A a → Choice B b →
+               Choice (A × B) (a ∧ b)
+ofʸ  a ×-choice ofʸ  b = of (a , b)
+ofʸ  a ×-choice ofⁿ ¬b = of (¬b ∘ proj₂)
+ofⁿ ¬a ×-choice _      = of (¬a ∘ proj₁)
+
+_⊎-choice_ : ∀ {a b} → Choice A a → Choice B b →
+               Choice (A ⊎ B) (a ∨ b)
+ofʸ  a ⊎-choice      _ = of (inj₁ a)
+ofⁿ ¬a ⊎-choice ofʸ  b = of (inj₂ b)
+ofⁿ ¬a ⊎-choice ofⁿ ¬b = of (¬a ¬-⊎ ¬b)
+
+_→-choice_ : ∀ {a b} → Choice A a → Choice B b →
+                Choice (A → B) (not a ∨ b)
+ofʸ  a →-choice ofʸ  b = of (const b)
+ofʸ  a →-choice ofⁿ ¬b = of (¬b ∘ (_$ a))
+ofⁿ ¬a →-choice _      = of (λ a → contradiction a ¬a)
+-}
+
+------------------------------------------------------------------------
+-- Other lemmas
+
+fromEquivalence : ∀ {b} → (T b → A) → (A → T b) → Reflects A b
+fromEquivalence {b = true}  sound complete = of (sound _)
+fromEquivalence {b = false} sound complete = of complete
+
+{-
+-- `Choice` is deterministic.
+det : ∀ {b b′} → Choice A b → Choice A b′ → b ≡ b′
+det (ofʸ  a) (ofʸ  _) = refl
+det (ofʸ  a) (ofⁿ ¬a) = contradiction a ¬a
+det (ofⁿ ¬a) (ofʸ  a) = contradiction a ¬a
+det (ofⁿ ¬a) (ofⁿ  _) = refl
+
+T-choice-elim : ∀ {a b} → Choice (T a) b → b ≡ a
+T-choice-elim {a} r = det r (T-choice a)
+-}
diff --git a/src/Relation/Nullary/Orthogonal.agda b/src/Relation/Nullary/Orthogonal.agda
new file mode 100644
index 0000000000..36ca8ffcdc
--- /dev/null
+++ b/src/Relation/Nullary/Orthogonal.agda
@@ -0,0 +1,128 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Orthogonality for types
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Nullary.Orthogonal where
+
+open import Data.Bool.Base as Bool using (T; true; false; not)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Empty.Polymorphic renaming (⊥ to ⊥ˡ; ⊥-elim to ⊥ˡ-elim)
+open import Data.Product.Base using (_×_; Σ-syntax; _,_; proj₁; proj₂)
+open import Data.Sum.Base using (_⊎_; [_,_]′)
+open import Data.Unit.Base using (⊤)
+
+open import Function.Base using (const; flip; _∘′_; _$′_)
+
+open import Level using (Level; _⊔_)
+
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+
+private
+  variable
+    a aⁿ b bⁿ p q : Level
+    A : Set a
+    ¬A : Set aⁿ
+    B : Set b
+    ¬B : Set bⁿ
+    P : Set p
+    Q : Set q
+
+------------------------------------------------------------------------
+-- Basic definitions
+
+-- Two types are orthogonal with respect to a pole P when assuming
+-- that both are inhabited leads to a proof of P.
+-- In particular, when the pole is the empty set this amounts to
+-- saying that one is a (more or less constructive) notiong of
+-- negation for the other.
+
+infix 1 _⫫[_]_
+record _⫫[_]_ (A : Set a) (P : Set p) (B : Set b) : Set (p ⊔ a ⊔ b) where
+  field orthogonal : A → B → P
+
+  co-orthogonal : B → A → P
+  co-orthogonal = flip orthogonal
+open _⫫[_]_ public
+
+------------------------------------------------------------------------
+-- Base cases
+
+-- The empty type is orthogonal with everything
+∅ : ⊥ ⫫[ P ] A
+∅ .orthogonal = ⊥-elim
+
+⊘ˡ : ⊥ˡ {a} ⫫[ P ] A
+⊘ˡ .orthogonal = ⊥ˡ-elim
+
+-- Truth of a boolean is orthogonal to truth of its negation
+Truth : ∀ b → Bool.T b ⫫[ P ] Bool.T (not b)
+Truth false .orthogonal = ⊥-elim
+Truth true  .orthogonal = flip ⊥-elim
+
+-- A type is always orthogonal to its negation
+negation : (A : Set a) → A ⫫[ P ] ¬ A
+negation A .orthogonal = contradiction
+
+-- If our notion of orthogonality is with respect to ⊤ then any
+-- two things are related
+universal : A ⫫[ ⊤ ] B
+universal .orthogonal = _
+
+------------------------------------------------------------------------
+-- Closure principles
+
+-- The relation is a contravariant bifunctor
+map : (B → A) → (P → Q) → (¬B → ¬A) → A ⫫[ P ] ¬A → B ⫫[ Q ] ¬B
+map f g ¬f oA .orthogonal b ¬b = g (oA .orthogonal (f b) (¬f ¬b))
+
+-- Being ⊥-orthogonal to the unit type is being uninhabited
+uninhabited : ⊤ ⫫[ ⊥ ] A → ¬ A
+uninhabited oA = oA .orthogonal _
+
+------------------------------------------------------------------------
+-- Type constructors building constructive negations
+
+-- Constructive negation just swaps the two parameters.
+-- It is involutive!
+∁ : A ⫫[ P ] ¬A → ¬A ⫫[ P ] A
+∁ oA .orthogonal a ¬a = oA .orthogonal ¬a a
+
+-- The negation of a function is a proof the domain is inhabited
+-- together with a negation of the codomain
+_⇒_ : (A : Set a) → B ⫫[ P ] ¬B → (A → B) ⫫[ P ] (A × ¬B)
+(oA ⇒ oB) .orthogonal f (a , ¬b) = oB .orthogonal (f a) ¬b
+
+Π : (A : Set a) {B : A → Set b} {¬B : A → Set bⁿ}
+  → ((a : A) → B a ⫫[ P ] ¬B a) → ((a : A) → B a) ⫫[ P ] (Σ[ a ∈ A ] ¬B a)
+Π A oB .orthogonal f (a , ¬b) = oB a .orthogonal (f a) ¬b
+
+-- The negation of a conjunction is a disjunction of negations
+_∩_ : A ⫫[ P ] ¬A → B ⫫[ P ] ¬B → (A × B) ⫫[ P ] (¬A ⊎ ¬B)
+(oA ∩ oB) .orthogonal (a , b) =
+  [ oA .orthogonal a
+  , oB .orthogonal b ]′
+
+Σ : A ⫫[ P ] ¬A → {B : A → Set b} {¬B : A → Set bⁿ} → ((a : A) → B a ⫫[ P ] ¬B a)
+  → (Σ[ a ∈ A ] B a) ⫫[ P ] (¬A ⊎ ((a : A) → ¬B a))
+Σ oA oB .orthogonal (a , b) =
+  [ oA .orthogonal a
+  , (λ f → oB a .orthogonal b (f a)) ]′
+
+-- The negation of a strict left-to-right conjunction is defined
+-- by either finding a way to disprove A or, a way to disprove B
+-- given the knowledge that A is provable
+_!∩_ : A ⫫[ P ] ¬A → B ⫫[ P ] ¬B → (A × B) ⫫[ P ] (¬A ⊎ (A × ¬B))
+(oA !∩ oB) .orthogonal (a , b) =
+  [ oA .orthogonal a
+  , oB .orthogonal b ∘′ proj₂ ]′
+
+
+-- The negation of a disjunction is a conjunction of negations
+-- This is defined using de Morgan's law
+
+_∪_ : A ⫫[ P ] ¬A → B ⫫[ P ] ¬B → (A ⊎ B) ⫫[ P ] (¬A × ¬B)
+oA ∪ oB = ∁ (∁ oA ∩ ∁ oB)