open Data.Nat using (_<_;s<s)
<-irrefl : ∀ { n : ℕ } → ¬ (n < n)
<-irrefl {zero} = λ()
<-irrefl {suc n} = λ{ (s<s n<n) → <-irrefl n<n }

open Data.Nat using (_>_;z<s;s≤s;z≤n)
open Relation.Binary.PropositionalEquality using (cong)
trichotomy : ∀ ( m n : ℕ )
  →   (m < n × ¬ m ≡ n × ¬ m > n)
  ⊎ (¬ m < n ×   m ≡ n × ¬ m > n)
  ⊎ (¬ m < n × ¬ m ≡ n ×   m > n)
trichotomy zero    zero    = inj₂ (inj₁ ⟨ (λ ()) , ⟨ refl , (λ ()) ⟩ ⟩)
trichotomy zero    (suc n) = inj₁ ⟨ (z<s) , ⟨ (λ ()) , (λ ()) ⟩ ⟩
trichotomy (suc m) zero    = inj₂ (inj₂ ⟨ (λ ()), ⟨ (λ ()), (z<s) ⟩ ⟩)
trichotomy (suc m) (suc n) with trichotomy m n
...| inj₁ ⟨ m<n , ⟨ ¬m≡n , ¬m>n ⟩ ⟩ =
     inj₁
       ⟨ s<s m<n
       , ⟨ (λ{ refl → ¬m≡n refl })
       , (λ{ (s<s m>n) → ¬m>n m>n }) ⟩
       ⟩
...| inj₂ (inj₁ ⟨ ¬m<n , ⟨ m≡n , ¬m>n ⟩ ⟩) =
     inj₂ (inj₁
       ⟨ (λ{ (s<s m<n) → ¬m<n m<n} )
       , ⟨ (cong suc m≡n)
       , (λ{ (s<s m>n) → ¬m>n m>n }) ⟩
       ⟩)
...| inj₂ (inj₂ ⟨ ¬m<n , ⟨ ¬m≡n , m>n ⟩ ⟩) =
     inj₂ (inj₂
       ⟨ (λ{ (s<s m<n) → ¬m<n m<n })
       , ⟨ (λ{ refl → ¬m≡n refl })
       , s<s m>n ⟩
       ⟩)

open import plfa.part1.Isomorphism using (_∘_)
-- Cannot import from Connectives as it's not using stdlib Sum and Product types!
→-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C))
→-distrib-⊎ =
  record
    { to      = λ{ f → ⟨ f ∘ inj₁ , f ∘ inj₂ ⟩ }
    ; from    = λ{ ⟨ g , h ⟩ → λ{ (inj₁ x) → g x ; (inj₂ y) → h y } }
    ; from∘to = λ{ f → extensionality λ{ (inj₁ x) → refl ; (inj₂ y) → refl } }
    ; to∘from = λ{ _ → refl }
    }
⊎-dual-× : ∀ {A B : Set} → ¬ (A ⊎ B) ≃ (¬ A) × (¬ B)
⊎-dual-× = →-distrib-⊎ {_} {_} {⊥}

```agda

-- Cannot do the other way around because `(¬ A) ⊎ (¬ B)` holds only iff ¬ A or
-- ¬ B exclusively, whereas `¬ (A × B)` may hold when both ¬ A and ¬ B hold
⊎-implies-× : ∀ {A B : Set} → (¬ A) ⊎ (¬ B) → ¬ (A × B)
⊎-implies-× = λ
  { (inj₁ ¬a) → ¬a ∘ proj₁
  ; (inj₂ ¬b) → ¬b ∘ proj₂
  }
```

em-implies-dne : ∀ {A : Set} → (A ⊎ ¬ A) → ¬ ¬ A → A
em-implies-dne (inj₁ a)  _   = a
em-implies-dne (inj₂ ¬a) ¬¬a = ⊥-elim (¬¬a ¬a) -- bottom implies anything
em-implies-pierce : ∀ {A B : Set} → (A ⊎ ¬ A) → ((A → B) → A) → A
em-implies-pierce (inj₁ a) _      = a
em-implies-pierce (inj₂ ¬a) a-b-a = a-b-a λ{ a → ⊥-elim (¬a a) }
em-implies-imdis : ∀ {A B : Set} → (A ⊎ ¬ A) → (A → B) → ¬ A ⊎ B
em-implies-imdis (inj₁ a) a-b  = inj₂ (a-b a)
em-implies-imdis (inj₂ ¬a) _   = inj₁ ¬a
em-implies-demorg : ∀ {A B : Set} → (∀ {C : Set} → C ⊎ ¬ C) → ¬ (¬ A × ¬ B) → A ⊎ B
em-implies-demorg {A} {B} em demorg-dom with em {A} | em {B}
...| inj₁ a  | _       = inj₁ a
...| inj₂ _  | inj₁ b  = inj₂ b
...| inj₂ ¬a | inj₂ ¬b = ⊥-elim (demorg-dom ⟨ ¬a , ¬b ⟩)
dne-implies-em : ∀ {A : Set} → ¬ ¬ A → A → (A ⊎ ¬ A)
dne-implies-em _ a = inj₁ a
dne-implies-pierce : ∀ {A B : Set} → ¬ ¬ A → A → ((A → B) → A) → A
dne-implies-pierce _ a = λ _ → a
dne-implies-imdis : ∀ {A B : Set} → ¬ ¬ A → A → (A → B) → ¬ A ⊎ B
dne-implies-imdis _ a = λ a→b → inj₂ (a→b a)
dne-implies-demorg : ∀ {A B : Set} → ¬ ¬ A → A → ¬ (¬ A × ¬ B) → A ⊎ B
dne-implies-demorg _ a = λ _ → inj₁ a
pierce-implies-em : ∀ {A B : Set} → ((A → B) → A) → A → (A ⊎ ¬ A)
pierce-implies-em _ a = inj₁ a
pierce-implies-dne : ∀ {A B : Set} → ((A → B) → A) → A → ¬ ¬ A → A
pierce-implies-dne _ a _ = a
pierce-implies-imdis : ∀ {A B : Set} → ((A → B) → A) → A → (A → B) → ¬ A ⊎ B
pierce-implies-imdis _ a a→b = inj₂ (a→b a)
pierce-implies-demorg : ∀ {A B : Set} → ((A → B) → A) → A → ¬ (¬ A × ¬ B) → A ⊎ B
pierce-implies-demorg _ a _ = inj₁ a
imdis-implies-em : (∀ {A B : Set} → (A → B) → ¬ A ⊎ B) → ∀ {C : Set} → (C ⊎ ¬ C)
imdis-implies-em imdis with (imdis λ{ a → a })
...| (inj₁ ¬a) = inj₂ ¬a
...| (inj₂ a)  = inj₁ a
imdis-implies-dne : (∀ {A B : Set} → (A → B) → ¬ A ⊎ B) → ∀ {C : Set} → ¬ ¬ C → C
imdis-implies-dne imdis ¬¬c with (imdis λ{ a → a })
...| (inj₁ ¬a) = ⊥-elim (¬¬c ¬a)
...| (inj₂ a)  = a
imdis-implies-pierce : ∀ {A B : Set} → (A → B) → ¬ A ⊎ B → ((A → B) → A) → A
imdis-implies-pierce a→b _ a→b→a = a→b→a a→b
imdis-implies-demorg : (∀ {A B : Set} → (A → B) → ¬ A ⊎ B) → ∀ {C D : Set} → ¬ (¬ C × ¬ D) → C ⊎ D
imdis-implies-demorg imdis {C} {D} demorg-dom with (imdis {C} λ{ a → a }) | (imdis {D} λ{ a → a })
... | _       | inj₂ d  = inj₂ d
... | inj₂ c  | _       = inj₁ c
... | inj₁ ¬c | inj₁ ¬d = ⊥-elim (demorg-dom ⟨ ¬c , ¬d ⟩)

¬-stable : {A : Set} → Stable (¬ A)
¬-stable = ¬¬¬-elim
×-stable : {A B : Set} → Stable A → Stable B → Stable (A × B)
×-stable a b ¬¬a×b =
  ⟨ (a (λ ¬¬a → ¬¬a×b (λ a×b → ¬¬a (proj₁ a×b))))
  , (b (λ ¬¬b → ¬¬a×b (λ a×b → ¬¬b (proj₂ a×b))))
  ⟩