From d24ce8c6e1f520bea548fddf781aa014fd26f9aa Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Fri, 26 Sep 2025 07:44:40 +0200
Subject: [PATCH 1/3] Add De Morgan's law for Pred

---
 CHANGELOG.md                       |  6 ++++++
 src/Relation/Unary/Properties.agda | 11 ++++++++++-
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 081dda5b66..28f77783d6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -103,3 +103,9 @@ Additions to existing modules
   ```agda
   ¬¬-η : A → ¬ ¬ A
   ```
+
+* In Relation.Unary.Properites
+  ```agda
+  ¬∃⟨P⟩⇒Π[∁P] : ¬ ∃⟨ P ⟩ → Π[ ∁ P ]
+  ¬∃⟨P⟩⇒∀[∁P] : ¬ ∃⟨ P ⟩ → ∀[ ∁ P ]
+  ```
diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda
index b16b6702b8..d0de3cc554 100644
--- a/src/Relation/Unary/Properties.agda
+++ b/src/Relation/Unary/Properties.agda
@@ -8,7 +8,7 @@
 
 module Relation.Unary.Properties where
 
-open import Data.Product.Base as Product using (_×_; _,_; swap; proj₁; zip′)
+open import Data.Product.Base as Product using (_×_; _,_; -,_; swap; proj₁; zip′)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Unit.Base using (tt)
 open import Function.Base using (id; _$_; _∘_; _∘₂_)
@@ -52,6 +52,15 @@ U-Universal = λ _ → _
 ∁U-Empty : Empty {A = A} (∁ U)
 ∁U-Empty = λ x x∈∁U → x∈∁U _
 
+------------------------------------------------------------------------
+-- De Morgan's law
+
+¬∃⟨P⟩⇒Π[∁P] : ∀ {P : Pred A ℓ} → ¬ ∃⟨ P ⟩ → Π[ ∁ P ]
+¬∃⟨P⟩⇒Π[∁P] ¬sat x Px = ¬sat (x , Px)
+
+¬∃⟨P⟩⇒∀[∁P] : ∀ {P : Pred A ℓ} → ¬ ∃⟨ P ⟩ → ∀[ ∁ P ]
+¬∃⟨P⟩⇒∀[∁P] ¬sat Px = ¬sat (-, Px)
+
 ------------------------------------------------------------------------
 -- Subset properties
 

From 0a974c5dd52df0d0c1a3c749bb5360afb67a4c07 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Fri, 26 Sep 2025 07:51:29 +0200
Subject: [PATCH 2/3] Add more of De Morgan's laws

---
 CHANGELOG.md                       |  4 ++++
 src/Relation/Unary/Properties.agda | 14 +++++++++++++-
 2 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 28f77783d6..67aa9cd9ff 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -108,4 +108,8 @@ Additions to existing modules
   ```agda
   ¬∃⟨P⟩⇒Π[∁P] : ¬ ∃⟨ P ⟩ → Π[ ∁ P ]
   ¬∃⟨P⟩⇒∀[∁P] : ¬ ∃⟨ P ⟩ → ∀[ ∁ P ]
+  ∃⟨∁P⟩⇒¬Π[P] : ∃⟨ ∁ P ⟩ → ¬ Π[ P ]
+  ∃⟨∁P⟩⇒¬∀[P] : ∃⟨ ∁ P ⟩ → ¬ ∀[ P ]
+  Π[∁P]⇒¬∃[P] : Π[ ∁ P ] → ¬ ∃⟨ P ⟩
+  ∀[∁P]⇒¬∃[P] : ∀[ ∁ P ] → ¬ ∃⟨ P ⟩
   ```
diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda
index d0de3cc554..118005f3e4 100644
--- a/src/Relation/Unary/Properties.agda
+++ b/src/Relation/Unary/Properties.agda
@@ -53,7 +53,7 @@ U-Universal = λ _ → _
 ∁U-Empty = λ x x∈∁U → x∈∁U _
 
 ------------------------------------------------------------------------
--- De Morgan's law
+-- De Morgan's laws
 
 ¬∃⟨P⟩⇒Π[∁P] : ∀ {P : Pred A ℓ} → ¬ ∃⟨ P ⟩ → Π[ ∁ P ]
 ¬∃⟨P⟩⇒Π[∁P] ¬sat x Px = ¬sat (x , Px)
@@ -61,6 +61,18 @@ U-Universal = λ _ → _
 ¬∃⟨P⟩⇒∀[∁P] : ∀ {P : Pred A ℓ} → ¬ ∃⟨ P ⟩ → ∀[ ∁ P ]
 ¬∃⟨P⟩⇒∀[∁P] ¬sat Px = ¬sat (-, Px)
 
+∃⟨∁P⟩⇒¬Π[P] : ∀ {P : Pred A ℓ} → ∃⟨ ∁ P ⟩ → ¬ Π[ P ]
+∃⟨∁P⟩⇒¬Π[P] (x , ¬Px) ΠP = ¬Px (ΠP x)
+
+∃⟨∁P⟩⇒¬∀[P] : ∀ {P : Pred A ℓ} → ∃⟨ ∁ P ⟩ → ¬ ∀[ P ]
+∃⟨∁P⟩⇒¬∀[P] (x , ¬Px) ∀P = ¬Px ∀P
+
+Π[∁P]⇒¬∃[P] : ∀ {P : Pred A ℓ} → Π[ ∁ P ] → ¬ ∃⟨ P ⟩
+Π[∁P]⇒¬∃[P] Π∁P (x , Px) = Π∁P x Px
+
+∀[∁P]⇒¬∃[P] : ∀ {P : Pred A ℓ} → ∀[ ∁ P ] → ¬ ∃⟨ P ⟩
+∀[∁P]⇒¬∃[P] ∀∁P (x , Px) = ∀∁P Px
+
 ------------------------------------------------------------------------
 -- Subset properties
 

From b406933e5afbb64ea571d4530435831ff0f3c6ed Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Fri, 26 Sep 2025 14:42:33 +0200
Subject: [PATCH 3/3] Don't name unused variables

---
 src/Relation/Unary/Properties.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda
index 118005f3e4..a8affa37ed 100644
--- a/src/Relation/Unary/Properties.agda
+++ b/src/Relation/Unary/Properties.agda
@@ -65,13 +65,13 @@ U-Universal = λ _ → _
 ∃⟨∁P⟩⇒¬Π[P] (x , ¬Px) ΠP = ¬Px (ΠP x)
 
 ∃⟨∁P⟩⇒¬∀[P] : ∀ {P : Pred A ℓ} → ∃⟨ ∁ P ⟩ → ¬ ∀[ P ]
-∃⟨∁P⟩⇒¬∀[P] (x , ¬Px) ∀P = ¬Px ∀P
+∃⟨∁P⟩⇒¬∀[P] (_ , ¬Px) ∀P = ¬Px ∀P
 
 Π[∁P]⇒¬∃[P] : ∀ {P : Pred A ℓ} → Π[ ∁ P ] → ¬ ∃⟨ P ⟩
 Π[∁P]⇒¬∃[P] Π∁P (x , Px) = Π∁P x Px
 
 ∀[∁P]⇒¬∃[P] : ∀ {P : Pred A ℓ} → ∀[ ∁ P ] → ¬ ∃⟨ P ⟩
-∀[∁P]⇒¬∃[P] ∀∁P (x , Px) = ∀∁P Px
+∀[∁P]⇒¬∃[P] ∀∁P (_ , Px) = ∀∁P Px
 
 ------------------------------------------------------------------------
 -- Subset properties