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 ⟩)))))
+```