response to review comments

Author: jamesmckinna

CHANGELOG.md

@@ -407,14 +407,19 @@ Additions to existing modules
   WeaklyDecidable : Set _
   ```
 
+* Added new proof in `Relation.Nullary.Decidable`:
+  ```agda
+  ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
+  ```
+
 * Added new definitions in `Relation.Nullary.Negation.Core`:
   ```agda
-  weak-contradiction : .A → ¬ A → Whatever
+  contradiction-irr : .A → ¬ A → Whatever
   ```
 
-* Added new proof in `Relation.Nullary.Decidable`:
+* Added new definitions in `Relation.Nullary.Reflects`:
   ```agda
-  ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
+  recompute : Reflects A b → Recomputable A
   ```
 
 * Added new definitions in `Relation.Unary`

src/Relation/Nullary/Negation/Core.agda

@@ -47,26 +47,26 @@ _¬-⊎_ = [_,_]
 ------------------------------------------------------------------------
 -- Uses of negation
 
-weak-contradiction : .A → ¬ A → Whatever
-weak-contradiction a ¬a = ⊥-elim-irr (¬a a)
+contradiction-irr : .A → ¬ A → Whatever
+contradiction-irr a ¬a = ⊥-elim-irr (¬a a)
 
 contradiction : A → ¬ A → Whatever
-contradiction a = weak-contradiction a
+contradiction a = contradiction-irr a
 
 contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever
-contradiction₂ (inj₁ a) ¬a ¬b = weak-contradiction a ¬a
-contradiction₂ (inj₂ b) ¬a ¬b = weak-contradiction b ¬b
+contradiction₂ (inj₁ a) ¬a ¬b = contradiction a ¬a
+contradiction₂ (inj₂ b) ¬a ¬b = contradiction b ¬b
 
 contraposition : (A → B) → ¬ B → ¬ A
-contraposition f ¬b a = weak-contradiction (f a) ¬b
+contraposition f ¬b a = contradiction (f a) ¬b
 
 -- Everything is stable in the double-negation monad.
 stable : ¬ ¬ Stable A
-stable ¬[¬¬a→a] = ¬[¬¬a→a] (weak-contradiction (¬[¬¬a→a] ∘ const))
+stable ¬[¬¬a→a] = ¬[¬¬a→a] (contradiction (¬[¬¬a→a] ∘ const))
 
 -- Negated predicates are stable.
 negated-stable : Stable (¬ A)
-negated-stable ¬¬¬a a = ¬¬¬a (weak-contradiction a)
+negated-stable ¬¬¬a a = ¬¬¬a (contradiction a)
 
 ¬¬-map : (A → B) → ¬ ¬ A → ¬ ¬ B
 ¬¬-map f = contraposition (contraposition f)

src/Relation/Nullary/Recomputable.agda

@@ -21,16 +21,19 @@ private
 
 ------------------------------------------------------------------------
 -- Definition
+--
+-- The idea of being 'recomputable' is that, given an *irrelevant* proof
+-- of a proposition `A` (signalled by being a value of type `.A`, all of
+-- whose inhabitants are identified up to definitional equality, and hence
+-- do *not* admit pattern-matching), one may 'promote' such a value to a
+-- 'genuine' value of `A`, available for subsequent eg. pattern-matching.
 
 Recomputable : (A : Set a) → Set a
 Recomputable A = .A → A
 
 ------------------------------------------------------------------------
 -- Constructions
 
-------------------------------------------------------------------------
--- Recomputable types are Harrop
-
 ⊥-recompute : Recomputable ⊥
 ⊥-recompute ()
 

src/Relation/Nullary/Reflects.agda

@@ -15,7 +15,8 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Level using (Level)
 open import Function.Base using (_$_; _∘_; const; id)
-open import Relation.Nullary.Negation.Core using (¬_; weak-contradiction; _¬-⊎_)
+open import Relation.Nullary.Negation.Core
+  using (¬_; contradiction-irr; contradiction; _¬-⊎_)
 open import Relation.Nullary.Recomputable using (Recomputable)
 
 private
@@ -58,7 +59,7 @@ invert (ofⁿ ¬a) = ¬a
 
 recompute : ∀ {b} → Reflects A b → Recomputable A
 recompute (ofʸ  a) _ = a
-recompute (ofⁿ ¬a) a = weak-contradiction a ¬a
+recompute (ofⁿ ¬a) a = contradiction-irr a ¬a
 
 ------------------------------------------------------------------------
 -- Interaction with negation, product, sums etc.
@@ -92,7 +93,7 @@ _→-reflects_ : ∀ {a b} → Reflects A a → Reflects B b →
                 Reflects (A → B) (not a ∨ b)
 ofʸ  a →-reflects ofʸ  b = of (const b)
 ofʸ  a →-reflects ofⁿ ¬b = of (¬b ∘ (_$ a))
-ofⁿ ¬a →-reflects _      = of (λ a → weak-contradiction a ¬a)
+ofⁿ ¬a →-reflects _      = of (λ a → contradiction a ¬a)
 
 ------------------------------------------------------------------------
 -- Other lemmas
@@ -104,8 +105,8 @@ fromEquivalence {b = false} sound complete = of complete
 -- `Reflects` is deterministic.
 det : ∀ {b b′} → Reflects A b → Reflects A b′ → b ≡ b′
 det (ofʸ  a) (ofʸ  _) = refl
-det (ofʸ  a) (ofⁿ ¬a) = weak-contradiction a ¬a
-det (ofⁿ ¬a) (ofʸ  a) = weak-contradiction a ¬a
+det (ofʸ  a) (ofⁿ ¬a) = contradiction a ¬a
+det (ofⁿ ¬a) (ofʸ  a) = contradiction a ¬a
 det (ofⁿ ¬a) (ofⁿ  _) = refl
 
 T-reflects-elim : ∀ {a b} → Reflects (T a) b → b ≡ a