From 847b270b6e30c07265214e1cfc8c4509960d8d04 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Tue, 26 Mar 2024 10:42:43 -0400 Subject: [PATCH 1/2] minor refactor: use Data.Unit.Polymorphic instead of an explicit Lift. --- src/Relation/Nullary/Decidable/Core.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda index f77613ea65..587b155716 100644 --- a/src/Relation/Nullary/Decidable/Core.agda +++ b/src/Relation/Nullary/Decidable/Core.agda @@ -13,14 +13,14 @@ module Relation.Nullary.Decidable.Core where open import Level using (Level; Lift) open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_) -open import Data.Unit.Base using (⊤) -open import Data.Empty using (⊥) +open import Data.Unit.Polymorphic.Base using (⊤) open import Data.Empty.Irrelevant using (⊥-elim) open import Data.Product.Base using (_×_) open import Data.Sum.Base using (_⊎_) open import Function.Base using (_∘_; const; _$_; flip) open import Relation.Nullary.Reflects open import Relation.Nullary.Negation.Core + using (¬_; Stable; negated-stable; contradiction; DoubleNegation) private variable @@ -58,11 +58,11 @@ module _ {A : Set a} where From-yes : Dec A → Set a From-yes (true because _) = A - From-yes (false because _) = Lift a ⊤ + From-yes (false because _) = ⊤ From-no : Dec A → Set a From-no (false because _) = ¬ A - From-no (true because _) = Lift a ⊤ + From-no (true because _) = ⊤ ------------------------------------------------------------------------ -- Recompute From 20dfc42b172ebf975b7601c5ceb191cc37992c3d Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Tue, 26 Mar 2024 10:43:07 -0400 Subject: [PATCH 2/2] additional tweak: use contradiction where possible. --- src/Relation/Nullary/Decidable/Core.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda index 587b155716..83da26e51b 100644 --- a/src/Relation/Nullary/Decidable/Core.agda +++ b/src/Relation/Nullary/Decidable/Core.agda @@ -171,7 +171,7 @@ proof (map′ A→B B→A (false because [¬a])) = ofⁿ (invert [¬a] ∘ B→A decidable-stable : Dec A → Stable A decidable-stable (yes a) ¬¬a = a -decidable-stable (no ¬a) ¬¬a = ⊥-elim (¬¬a ¬a) +decidable-stable (no ¬a) ¬¬a = contradiction ¬a ¬¬a ¬-drop-Dec : Dec (¬ ¬ A) → Dec (¬ A) ¬-drop-Dec ¬¬a? = map′ negated-stable contradiction (¬? ¬¬a?)