[ add ] flipped version of Relation.Nullary.Negation.Core.contradiction

CHANGELOG.md

@@ -20,6 +20,9 @@ Minor improvements
 * The type of `Relation.Nullary.Negation.Core.contradiction-irr` has been further
   weakened so that the negated hypothesis `¬ A` is marked as irrelevant. This is
   safe to do, in view of `Relation.Nullary.Recomputable.Properties.¬-recompute`.
+  Furthermore, because the *eager* insertion of implicit arguments during type
+  inference interacts badly with `contradiction`, we introduce an explicit name
+  `contradiction′` for its `flip`ped version.
 
 * Refactored usages of `+-∸-assoc 1` to `∸-suc` in:
   ```agda
@@ -101,5 +104,6 @@ Additions to existing modules
 
 * In `Relation.Nullary.Negation.Core`
   ```agda
-  ¬¬-η : A → ¬ ¬ A
+  ¬¬-η           : A → ¬ ¬ A
+  contradiction′ : ¬ A → A → Whatever
   ```

src/Relation/Nullary/Negation.agda

@@ -72,7 +72,7 @@ open import Relation.Nullary.Negation.Core public
 -- ⊥).
 
 call/cc : ((A → Whatever) → DoubleNegation A) → DoubleNegation A
-call/cc hyp ¬a = hyp (flip contradiction ¬a) ¬a
+call/cc hyp ¬a = hyp (contradiction′ ¬a) ¬a
 
 -- The "independence of premise" rule, in the double-negation monad.
 -- It is assumed that the index set (A) is inhabited.
@@ -82,7 +82,7 @@ independence-of-premise {A = A} {B = B} {P = P} q f = ¬¬-map helper ¬¬-exclu
   where
   helper : Dec B → Σ[ x ∈ A ] (B → P x)
   helper (yes p) = Product.map₂ const (f p)
-  helper (no ¬p) = (q , flip contradiction ¬p)
+  helper (no ¬p) = (q , contradiction′ ¬p)
 
 -- The independence of premise rule for binary sums.
 
@@ -91,7 +91,7 @@ independence-of-premise-⊎ {A = A} {B = B} {C = C} f = ¬¬-map helper ¬¬-exc
   where
   helper : Dec A → (A → B) ⊎ (A → C)
   helper (yes p) = Sum.map const const (f p)
-  helper (no ¬p) = inj₁ (flip contradiction ¬p)
+  helper (no ¬p) = inj₁ (contradiction′ ¬p)
 
 private
 

src/Relation/Nullary/Negation/Core.agda

@@ -58,6 +58,9 @@ contradiction-irr a ¬a = ⊥-elim-irr (¬a a)
 contradiction : A → ¬ A → Whatever
 contradiction a ¬a = contradiction-irr a ¬a
 
+contradiction′ : ¬ A → A → Whatever
+contradiction′ ¬a a = contradiction-irr a ¬a
+
 contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever
 contradiction₂ (inj₁ a) ¬a ¬b = contradiction a ¬a
 contradiction₂ (inj₂ b) ¬a ¬b = contradiction b ¬b