diff --git a/src/Relation/Nullary/Choice.agda b/src/Relation/Nullary/Choice.agda
new file mode 100644
index 0000000000..f24fb3d392
--- /dev/null
+++ b/src/Relation/Nullary/Choice.agda
@@ -0,0 +1,200 @@
+------------------------------------------------------------------------
+-- 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; ⊥-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 q : Level
+    A : Set ℓa
+    ¬A : Set ℓaⁿ
+    B : Set ℓb
+    ¬B : Set ℓbⁿ
+    P : Set p
+    Q : Set q
+    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 = 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 Q ¬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 Q ¬A oB b
+map₁ f = map f id
+
+map₂ : (¬A → ¬B) → Choice A P ¬A oA b → Choice A Q ¬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)
+
+_⊎-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ʸ (inj₁ a)
+ofⁿ ¬a ⊎-choice ofʸ  b = ofʸ (inj₂ b)
+ofⁿ ¬a ⊎-choice ofⁿ ¬b = ofⁿ (¬a , ¬b)
+
+_→-choice_ : Choice A B ¬A oA a → Choice B P ¬B oB b →
+             Choice (A → B) P (A × ¬B) (A ⇒ oB) (not a ∨ b)
+ofʸ  a →-choice ofʸ  b = ofʸ (const b)
+ofʸ  a →-choice ofⁿ ¬b = ofⁿ (a , ¬b)
+_→-choice_ {oA = oA} (ofⁿ ¬a) _ = ofʸ (λ a → oA .orthogonal 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 on orthogonal types.
+det : ∀ {b b′} → Choice A ⊥ ¬A oA b → Choice A ⊥ ¬A oA b′ → b ≡ b′
+det (ofʸ  a) (ofʸ  _) = refl
+det {oA = oA} (ofʸ  a) (ofⁿ ¬a) = ⊥-elim (oA .orthogonal a ¬a)
+det {oA = oA} (ofⁿ ¬a) (ofʸ  a) = ⊥-elim (oA .orthogonal a ¬a)
+det (ofⁿ ¬a) (ofⁿ  _) = refl
+
+T-reflects-elim : ∀ {a b} → Reflects (T a) b → b ≡ a
+T-reflects-elim {a} r = det r (T-reflects a)
diff --git a/src/Relation/Nullary/Choice2.agda b/src/Relation/Nullary/Choice2.agda
new file mode 100644
index 0000000000..a56bd9b603
--- /dev/null
+++ b/src/Relation/Nullary/Choice2.agda
@@ -0,0 +1,196 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of the `Choice` construct
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Nullary.Choice2 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; ⊥-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; ⊥-recompute)
+
+
+open import Relation.Nullary.Orthogonal
+  using (_⫫[_]_; byOrthogonality)
+
+private
+  variable
+    ℓa ℓaⁿ ℓb ℓbⁿ : Level
+    A : Set ℓa
+    ¬A : Set ℓaⁿ
+    B : Set ℓb
+    ¬B : Set ℓ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) (B : Set ℓb) : Bool → Set (ℓa ⊔ ℓb) where
+  ofʸ : (a : A) → Choice A B true
+  ofⁿ : (a : B) → Choice A B false
+
+Reflects : Set ℓa → Bool → Set ℓa
+Reflects A = Choice A (¬ 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 B b
+of {b = true } a = ofʸ a
+of {b = false} b = ofⁿ b
+
+invert : ∀ {b} → Choice A B b → if b then A else B
+invert (ofʸ a) = a
+invert (ofⁿ b) = b
+
+------------------------------------------------------------------------
+-- Transformation
+
+map : (A → B) → (¬A → ¬B) → Choice A ¬A b → Choice B ¬B b
+map f g (ofʸ a) = ofʸ (f a)
+map f g (ofⁿ b) = ofⁿ (g b)
+
+map₁ : (A → B) → Choice A ¬A b → Choice B ¬A b
+map₁ f = map f id
+
+map₂ : (¬A → ¬B) → Choice A ¬A b → Choice A ¬B 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 : {{oA : A ⫫[ ⊥ ] B}} → Choice A B b → Recomputable A
+recompute (ofʸ a) _ = a
+recompute (ofⁿ b) a = ⊥-elim-irr (byOrthogonality a b)
+
+recompute-constant :
+  {{oA : A ⫫[ ⊥ ] B}} (r : Choice A B 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 (¬ (⊥ˡ {ℓb})) false
+⊥ˡ-choice = ofⁿ λ ()
+
+⊥ˡ-reflects : Reflects (⊥ˡ {ℓa}) false
+⊥ˡ-reflects = ⊥ˡ-choice
+
+⊤ˡ-choice : Choice (⊤ˡ {ℓa}) B true
+⊤ˡ-choice = ofʸ _
+
+⊤ˡ-reflects : Reflects (⊤ˡ {ℓa}) true
+⊤ˡ-reflects = ⊤ˡ-choice
+
+⊥-choice : Choice A (¬ ⊥) false
+⊥-choice = ofⁿ λ ()
+
+⊥-reflects : Reflects ⊥ false
+⊥-reflects = ⊥-choice
+
+⊤-choice : Choice ⊤ B true
+⊤-choice = ofʸ _
+
+⊤-reflects : Reflects ⊤ true
+⊤-reflects = ⊤-choice
+
+∁-choice : Choice A B b → Choice B A (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
+
+T-choice : (b : Bool) → Choice (T b) (T (not b)) b
+T-choice true  = ⊤-choice
+T-choice false = ∁-choice ⊤-choice
+
+-- This could also be implemented using map over T-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 ¬A a → Choice B ¬B b →
+             Choice (A × B) (¬A ⊎ ¬B) (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 ¬A a → Choice B ¬B b →
+              Choice (A × B) (¬A ⊎ (A × ¬B)) (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)
+
+_⊎-choice_ : Choice A ¬A a → Choice B ¬B b  →
+             Choice (A ⊎ B) (¬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_ :
+  {{oA : A ⫫[ ⊥ ] ¬A}} →
+  Choice A ¬A a → Choice B ¬B b →
+  Choice (A → B) (A × ¬B) (not a ∨ b)
+ofʸ  a →-choice ofʸ  b = ofʸ (const b)
+ofʸ  a →-choice ofⁿ ¬b = ofⁿ (a , ¬b)
+ofⁿ ¬a →-choice _      = ofʸ (λ a → byOrthogonality 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 on orthogonal types.
+det : {{oA : A ⫫[ ⊥ ] ¬A}} → Choice A ¬A a → Choice A ¬A b → a ≡ b
+det (ofʸ  a) (ofʸ  _) = refl
+det (ofʸ  a) (ofⁿ ¬a) = byOrthogonality a ¬a
+det (ofⁿ ¬a) (ofʸ  a) = byOrthogonality a ¬a
+det (ofⁿ ¬a) (ofⁿ  _) = refl
+
+T-reflects-elim : Reflects (T a) b → b ≡ a
+T-reflects-elim {a} r = det r (T-reflects a)
diff --git a/src/Relation/Nullary/Choose/Core.agda b/src/Relation/Nullary/Choose/Core.agda
new file mode 100644
index 0000000000..8f39b61a87
--- /dev/null
+++ b/src/Relation/Nullary/Choose/Core.agda
@@ -0,0 +1,238 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Operations on and properties of decidable relations
+--
+-- This file contains some core definitions which are re-exported by
+-- Relation.Nullary.Choose
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Nullary.Choose.Core where
+
+{-
+open import Agda.Builtin.Equality using (_≡_)
+open import Agda.Builtin.Maybe using (Maybe; just; nothing)
+open import Level using (Level)
+open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
+open import Data.Unit.Polymorphic.Base using (⊤)
+open import Data.Empty.Polymorphic using (⊥)
+open import Data.Product.Base using (_×_)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Function.Base using (_∘_; const; _$_; flip)
+open import Relation.Nullary.Irrelevant using (Irrelevant)
+open import Relation.Nullary.Recomputable.Core as Recomputable
+  using (Recomputable)
+open import Relation.Nullary.Reflects as Reflects
+  hiding (recompute; recompute-constant)
+open import Relation.Nullary.Negation.Core
+  using (¬_; ¬¬-η; Stable; negated-stable; contradiction; DoubleNegation)
+-}
+
+open import Data.Bool.Base using (Bool; true; false)
+
+open import Relation.Nullary.Orthogonal using (_⫫[_]_)
+open import Relation.Nullary.Choice2 as Choice
+
+open import Level using (Level; _⊔_)
+
+private
+  variable
+    ℓa ℓaⁿ ℓb ℓbⁿ p q : Level
+    A : Set ℓa
+    ¬A : Set ℓaⁿ
+    B : Set ℓb
+    ¬B : Set ℓbⁿ
+    a b : Bool
+
+------------------------------------------------------------------------
+-- Definition.
+
+-- Decidability proofs have two parts: the `does` term which contains
+-- the boolean result and the `proof` term which contains a proof that
+-- reflects the boolean result. This definition allows the boolean
+-- part of the decision procedure to compute independently from the
+-- proof. This leads to better computational behaviour when we only care
+-- about the result and not the proof. See README.Design.Decidability
+-- for further details.
+
+infix 2 _because_
+
+record Choose (A : Set ℓa) (¬A : Set ℓaⁿ) : Set (ℓa ⊔ ℓaⁿ) where
+  constructor _because_
+  field
+    does  : Bool
+    proof : Choice A ¬A does
+
+open Choose public
+
+pattern yes a =  true because ofʸ  a
+pattern no ¬a = false because ofⁿ ¬a
+
+{-
+------------------------------------------------------------------------
+-- Flattening
+
+module _ {A : Set ℓa} {P : Set p} {¬A : Set ℓaⁿ} {oA : A ⫫[ P ] ¬A} where
+
+  From-yes : Choose A P ¬A oA → Set a
+  From-yes (true  because _) = A
+  From-yes (false because _) = ⊤
+
+  From-no : Choose A P ¬A oA → Set a
+  From-no (false because _) = ¬ A
+  From-no (true  because _) = ⊤
+
+------------------------------------------------------------------------
+-- Recompute
+
+-- Given an irrelevant proof of a decidable type, a proof can
+-- be recomputed and subsequently used in relevant contexts.
+
+recompute : Dec A → Recomputable A
+recompute = Reflects.recompute ∘ proof
+
+recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
+recompute-constant = Recomputable.recompute-constant ∘ recompute
+
+recompute-irrelevant-id : (a? : Dec A) → Irrelevant A → (a : A) → recompute a? a ≡ a
+recompute-irrelevant-id = Recomputable.recompute-irrelevant-id ∘ recompute
+
+------------------------------------------------------------------------
+-- Interaction with negation, sum, product etc.
+
+infixr 1 _⊎?_
+infixr 2 _×?_ _→?_
+
+T? : ∀ x → Dec (T x)
+T? x = x because T-reflects x
+
+¬? : Dec A → Dec (¬ A)
+does  (¬? a?) = not (does a?)
+proof (¬? a?) = ¬-reflects (proof a?)
+
+⊤? : Dec {a} ⊤
+does  ⊤? = true
+proof ⊤? = ⊤-reflects
+
+_×?_ : Dec A → Dec B → Dec (A × B)
+does  (a? ×? b?) = does a? ∧ does b?
+proof (a? ×? b?) = proof a? ×-reflects proof b?
+
+⊥? : Dec {a} ⊥
+does  ⊥?  = false
+proof ⊥?  = ⊥-reflects
+
+_⊎?_ : Dec A → Dec B → Dec (A ⊎ B)
+does  (a? ⊎? b?) = does a? ∨ does b?
+proof (a? ⊎? b?) = proof a? ⊎-reflects proof b?
+
+_→?_ : Dec A → Dec B → Dec (A → B)
+does  (a? →? b?) = not (does a?) ∨ does b?
+proof (a? →? b?) = proof a? →-reflects proof b?
+
+------------------------------------------------------------------------
+-- Relationship with Maybe
+
+dec⇒maybe : Dec A → Maybe A
+dec⇒maybe ( true because [a]) = just (invert [a])
+dec⇒maybe (false because  _ ) = nothing
+
+------------------------------------------------------------------------
+-- Relationship with Sum
+
+toSum : Dec A → A ⊎ ¬ A
+toSum ( true because  [p]) = inj₁ (invert  [p])
+toSum (false because [¬p]) = inj₂ (invert [¬p])
+
+fromSum : A ⊎ ¬ A → Dec A
+fromSum (inj₁ p)  = yes p
+fromSum (inj₂ ¬p) = no ¬p
+
+------------------------------------------------------------------------
+-- Relationship with booleans
+
+-- `isYes` is a stricter version of `does`. The lack of computation
+-- means that we can recover the proposition `P` from `isYes a?` by
+-- unification. This is useful when we are using the decision procedure
+-- for proof automation.
+
+isYes : Dec A → Bool
+isYes (true  because _) = true
+isYes (false because _) = false
+
+isNo : Dec A → Bool
+isNo = not ∘ isYes
+
+True : Dec A → Set
+True = T ∘ isYes
+
+False : Dec A → Set
+False = T ∘ isNo
+
+-- The traditional name for isYes is ⌊_⌋, indicating the stripping of evidence.
+⌊_⌋ = isYes
+
+------------------------------------------------------------------------
+-- Witnesses
+
+-- Gives a witness to the "truth".
+toWitness : {a? : Dec A} → True a? → A
+toWitness {a? = true  because [a]} _  = invert [a]
+toWitness {a? = false because  _ } ()
+
+-- Establishes a "truth", given a witness.
+fromWitness : {a? : Dec A} → A → True a?
+fromWitness {a? = true  because   _ } = const _
+fromWitness {a? = false because [¬a]} = invert [¬a]
+
+-- Variants for False.
+toWitnessFalse : {a? : Dec A} → False a? → ¬ A
+toWitnessFalse {a? = true  because   _ } ()
+toWitnessFalse {a? = false because [¬a]} _  = invert [¬a]
+
+fromWitnessFalse : {a? : Dec A} → ¬ A → False a?
+fromWitnessFalse {a? = true  because [a]} = flip _$_ (invert [a])
+fromWitnessFalse {a? = false because  _ } = const _
+
+-- If a decision procedure returns "yes", then we can extract the
+-- proof using from-yes.
+from-yes : (a? : Dec A) → From-yes a?
+from-yes (true  because [a]) = invert [a]
+from-yes (false because _ ) = _
+
+-- If a decision procedure returns "no", then we can extract the proof
+-- using from-no.
+from-no : (a? : Dec A) → From-no a?
+from-no (false because [¬a]) = invert [¬a]
+from-no (true  because   _ ) = _
+
+------------------------------------------------------------------------
+-- Maps
+
+map′ : (A → B) → (B → A) → Dec A → Dec B
+does  (map′ A→B B→A a?)                   = does a?
+proof (map′ A→B B→A (true  because  [a])) = of (A→B (invert [a]))
+proof (map′ A→B B→A (false because [¬a])) = of (invert [¬a] ∘ B→A)
+
+------------------------------------------------------------------------
+-- Relationship with double-negation
+
+-- Decidable predicates are stable.
+
+decidable-stable : Dec A → Stable A
+decidable-stable (true  because  [a]) ¬¬a = invert [a]
+decidable-stable (false because [¬a]) ¬¬a = contradiction (invert [¬a]) ¬¬a
+
+¬-drop-Dec : Dec (¬ ¬ A) → Dec (¬ A)
+¬-drop-Dec ¬¬a? = map′ negated-stable ¬¬-η (¬? ¬¬a?)
+
+-- A double-negation-translated variant of excluded middle (or: every
+-- nullary relation is decidable in the double-negation monad).
+
+¬¬-excluded-middle : DoubleNegation (Dec A)
+¬¬-excluded-middle ¬?a = ¬?a (no (λ a → ¬?a (yes a)))
+
+
+-}
diff --git a/src/Relation/Nullary/Orthogonal.agda b/src/Relation/Nullary/Orthogonal.agda
new file mode 100644
index 0000000000..725a51a1cf
--- /dev/null
+++ b/src/Relation/Nullary/Orthogonal.agda
@@ -0,0 +1,133 @@
+------------------------------------------------------------------------
+-- 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
+
+byOrthogonality : {{A ⫫[ ⊥ ] ¬A}} → A → ¬A → B
+byOrthogonality {{oA}} a ¬a = ⊥-elim (oA .orthogonal a ¬a)
+
+------------------------------------------------------------------------
+-- 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
+instance
+
+  negation : A ⫫[ P ] ¬ A
+  negation .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)