[ add ] eta law for ¬¬ monad

CHANGELOG.md

@@ -77,3 +77,8 @@ Additions to existing modules
   ≟-≢   : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n
   ∸-suc : m ≤ n → suc n ∸ m ≡ suc (n ∸ m)
   ```
+
+* In `Relation.Nullary.Negation.Core`
+  ```agda
+  ¬¬-η : A → ¬ ¬ A
+  ```

src/Data/List/Relation/Unary/First/Properties.agda

@@ -18,7 +18,7 @@ import Data.Sum.Base as Sum
 open import Function.Base using (_∘′_; _∘_; id)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; _≗_)
 open import Relation.Nullary.Decidable.Core as Dec
-open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Nullary.Negation.Core using (¬¬-η; contradiction)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Unary using (Pred; _⊆_; ∁; Irrelevant; Decidable)
 
@@ -54,7 +54,7 @@ module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
 module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
 
   All⇒¬First : P ⊆ ∁ Q → All P ⊆ ∁ (First P Q)
-  All⇒¬First p⇒¬q (px ∷ pxs) [ qx ]   = contradiction qx (p⇒¬q px)
+  All⇒¬First p⇒¬q (px ∷ pxs) [ qx ]   = p⇒¬q px qx
   All⇒¬First p⇒¬q (_ ∷ pxs)  (_ ∷ hf) = All⇒¬First p⇒¬q pxs hf
 
   First⇒¬All : Q ⊆ ∁ P → First P Q ⊆ ∁ (All P)
@@ -97,7 +97,7 @@ module _ {a p} {A : Set a} {P : Pred A p} where
 
   first? : Decidable P → Decidable (First P (∁ P))
   first? P? = Dec.fromSum
-            ∘ Sum.map₂ (All⇒¬First contradiction)
+            ∘ Sum.map₂ (All⇒¬First ¬¬-η)
             ∘ first (Dec.toSum ∘ P?)
 
   cofirst? : Decidable P → Decidable (First (∁ P) P)

src/Relation/Nullary/Decidable/Core.agda

@@ -28,7 +28,7 @@ open import Relation.Nullary.Recomputable.Core as Recomputable
 open import Relation.Nullary.Reflects as Reflects
   hiding (recompute; recompute-constant)
 open import Relation.Nullary.Negation.Core
-  using (¬_; Stable; negated-stable; contradiction; DoubleNegation)
+  using (¬_; ¬¬-η; Stable; negated-stable; contradiction; DoubleNegation)
 
 
 private
@@ -215,7 +215,7 @@ decidable-stable (true  because  [a]) ¬¬a = invert [a]
 decidable-stable (false because [¬a]) ¬¬a = contradiction (invert [¬a]) ¬¬a
 
 ¬-drop-Dec : Dec (¬ ¬ A) → Dec (¬ A)
-¬-drop-Dec ¬¬a? = map′ negated-stable contradiction (¬? ¬¬a?)
+¬-drop-Dec ¬¬a? = map′ negated-stable ¬¬-η (¬? ¬¬a?)
 
 -- A double-negation-translated variant of excluded middle (or: every
 -- nullary relation is decidable in the double-negation monad).

src/Relation/Nullary/Negation.agda

@@ -56,7 +56,7 @@ open import Relation.Nullary.Negation.Core public
 ¬¬-Monad : RawMonad {a} DoubleNegation
 ¬¬-Monad = mkRawMonad
   DoubleNegation
-  contradiction
+  ¬¬-η
   (λ x f → negated-stable (¬¬-map f x))
 
 ¬¬-push : DoubleNegation Π[ P ] → Π[ DoubleNegation ∘ P ]

src/Relation/Nullary/Negation/Core.agda

@@ -15,7 +15,7 @@ open import Level using (Level; _⊔_)
 
 private
   variable
-    a p q w : Level
+    a w : Level
     A B C : Set a
     Whatever : Set w
 
@@ -33,6 +33,11 @@ infix 3 ¬_
 DoubleNegation : Set a → Set a
 DoubleNegation A = ¬ ¬ A
 
+-- Eta law for double-negation
+
+¬¬-η : A → ¬ ¬ A
+¬¬-η a ¬a = ¬a a
+
 -- Stability under double-negation.
 Stable : Set a → Set a
 Stable A = ¬ ¬ A → A