From d5f810fa23b6c576c78535b84c2f62c649daf629 Mon Sep 17 00:00:00 2001
From: Philip Wadler <wadler@inf.ed.ac.uk>
Date: Sun, 10 Nov 2024 20:52:42 +0000
Subject: [PATCH] added DeMorgan to extra (#1063)

---
 extra/DeMorgan.lagda.md | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 extra/DeMorgan.lagda.md

diff --git a/extra/DeMorgan.lagda.md b/extra/DeMorgan.lagda.md
new file mode 100644
index 000000000..33f9aeb02
--- /dev/null
+++ b/extra/DeMorgan.lagda.md
@@ -0,0 +1,17 @@
+```
+module DeMorgan where
+
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Data.Nat using (ℕ; zero; suc)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
+open import Relation.Nullary.Negation using (¬_; contradiction)
+open import plfa.part1.Isomorphism using (_≃_; extensionality)
+
+postulate
+  dne : ∀ {A : Set} → ¬ ¬ A → A
+
+dm : ∀ {A B : Set} → ¬ (A × B) → (¬ A) ⊎ (¬ B)
+dm ¬xy = dne (λ k → k (inj₁ (λ x → k (inj₂ (λ y → ¬xy ⟨ x , y ⟩)))))
+```