From 22ed9358fce1757ad54b7ed5a5819d7e01801b70 Mon Sep 17 00:00:00 2001
From: Matthew <matthewdaggitt@gmail.com>
Date: Mon, 3 Jul 2017 22:16:16 +0100
Subject: [PATCH] =?UTF-8?q?Added=20`P-resp=E2=9F=B6=C2=ACP-resp`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                          | 5 +++++
 src/Relation/Binary/Consequences.agda | 5 +++++
 2 files changed, 10 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 494cfbb6a5..8795b734a6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -460,6 +460,11 @@ Backwards compatible changes
   All₂-concat⁻ : All₂ _~_ (concat xss) (concat yss) → All₂ (All₂ _~_) xss yss
   ```
 
+* Added proofs to `Relation.Binary.Consequences`
+  ```agda
+  P-resp⟶¬P-resp : Symmetric _≈_ → P Respects _≈_ → (¬_ ∘ P) Respects _≈_
+  ```
+
 Version 0.13
 ============
 
diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index 4b0f071eae..dafdc88161 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/src/Relation/Binary/Consequences.agda
@@ -114,6 +114,11 @@ trans∧tri⟶resp≈ {_≈_ = _≈_} {_<_} sym trans <-trans tri =
   ... | tri≈ _ y≈z _ = ⊥-elim (tri⟶irr tri (trans x≈y y≈z) x<z)
   ... | tri> _ _ z<y = ⊥-elim (tri⟶irr tri x≈y (<-trans x<z z<y))
 
+P-resp⟶¬P-resp :
+  ∀ {a p ℓ} {A : Set a} {_≈_ : Rel A ℓ} {P : A → Set p} →
+  Symmetric _≈_ → P Respects _≈_ → (¬_ ∘ P) Respects _≈_
+P-resp⟶¬P-resp sym resp x≈y ¬Px Py = ¬Px (resp (sym x≈y) Py)
+
 tri⟶dec≈ :
   ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
   Trichotomous _≈_ _<_ → Decidable _≈_