De Morgan's laws for Pred

CHANGELOG.md

@@ -103,3 +103,13 @@ Additions to existing modules
   ```agda
   ¬¬-η : A → ¬ ¬ A
   ```
+
+* In Relation.Unary.Properites
+  ```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 ⟩
+  ```

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,27 @@ U-Universal = λ _ → _
 ∁U-Empty : Empty {A = A} (∁ U)
 ∁U-Empty = λ x x∈∁U → x∈∁U _
 
+------------------------------------------------------------------------
+-- De Morgan's laws
+
+¬∃⟨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)
+
+∃⟨∁P⟩⇒¬Π[P] : ∀ {P : Pred A ℓ} → ∃⟨ ∁ P ⟩ → ¬ Π[ P ]
+∃⟨∁P⟩⇒¬Π[P] (x , ¬Px) ΠP = ¬Px (ΠP x)
+
+∃⟨∁P⟩⇒¬∀[P] : ∀ {P : Pred A ℓ} → ∃⟨ ∁ P ⟩ → ¬ ∀[ 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 (_ , Px) = ∀∁P Px
+
 ------------------------------------------------------------------------
 -- Subset properties