From 8f6987fde4e826cd6ee5e2153798b8a73f1db2ae Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 8 Apr 2024 12:13:08 +0100 Subject: [PATCH] knock-on, plus proof of `UIP` from #2149 --- CHANGELOG.md | 6 ++-- src/Axiom/UniquenessOfIdentityProofs.agda | 36 +++++++++++------------ src/Relation/Nullary.agda | 2 +- src/Relation/Nullary/Decidable/Core.agda | 4 +-- src/Relation/Nullary/Reflects.agda | 4 +-- 5 files changed, 25 insertions(+), 27 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index c19d0d327e..990474185b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -409,7 +409,7 @@ Additions to existing modules * Added new proof in `Relation.Nullary.Decidable.Core`: ```agda - recompute-irr : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q + recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q ``` * Added new proof in `Relation.Nullary.Decidable`: @@ -424,8 +424,8 @@ Additions to existing modules * Added new definitions in `Relation.Nullary.Reflects`: ```agda - recompute : Reflects A b → Recomputable A - recompute-irr : (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q + recompute : Reflects A b → Recomputable A + recompute-constant : (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q ``` * Added new definitions in `Relation.Unary` diff --git a/src/Axiom/UniquenessOfIdentityProofs.agda b/src/Axiom/UniquenessOfIdentityProofs.agda index 1cefc1a6a1..f64a700ae0 100644 --- a/src/Axiom/UniquenessOfIdentityProofs.agda +++ b/src/Axiom/UniquenessOfIdentityProofs.agda @@ -8,15 +8,19 @@ module Axiom.UniquenessOfIdentityProofs where -open import Data.Bool.Base using (true; false) -open import Data.Empty -open import Relation.Nullary.Reflects using (invert) -open import Relation.Nullary hiding (Irrelevant) +open import Level using (Level) +open import Relation.Nullary.Decidable.Core using (recompute; recompute-irr) open import Relation.Binary.Core open import Relation.Binary.Definitions open import Relation.Binary.PropositionalEquality.Core open import Relation.Binary.PropositionalEquality.Properties +private + variable + a : Level + A : Set a + x y : A + ------------------------------------------------------------------------ -- Definition -- @@ -24,7 +28,7 @@ open import Relation.Binary.PropositionalEquality.Properties -- equality are themselves equal. In other words, the equality relation -- is irrelevant. Here we define UIP relative to a given type. -UIP : ∀ {a} (A : Set a) → Set a +UIP : (A : Set a) → Set a UIP A = Irrelevant {A = A} _≡_ ------------------------------------------------------------------------ @@ -39,11 +43,11 @@ UIP A = Irrelevant {A = A} _≡_ -- the image of any other proof. module Constant⇒UIP - {a} {A : Set a} (f : _≡_ {A = A} ⇒ _≡_) - (f-constant : ∀ {a b} (p q : a ≡ b) → f p ≡ f q) + (f : _≡_ {A = A} ⇒ _≡_) + (f-constant : ∀ {x y} (p q : x ≡ y) → f p ≡ f q) where - ≡-canonical : ∀ {a b} (p : a ≡ b) → trans (sym (f refl)) (f p) ≡ p + ≡-canonical : (p : x ≡ y) → trans (sym (f refl)) (f p) ≡ p ≡-canonical refl = trans-symˡ (f refl) ≡-irrelevant : UIP A @@ -59,19 +63,13 @@ module Constant⇒UIP -- function over proofs of equality which is constant: it returns the -- proof produced by the decision procedure. -module Decidable⇒UIP - {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_) - where +module Decidable⇒UIP (_≟_ : Decidable {A = A} _≡_) where ≡-normalise : _≡_ {A = A} ⇒ _≡_ - ≡-normalise {a} {b} a≡b with a ≟ b - ... | true because [p] = invert [p] - ... | false because [¬p] = ⊥-elim (invert [¬p] a≡b) - - ≡-normalise-constant : ∀ {a b} (p q : a ≡ b) → ≡-normalise p ≡ ≡-normalise q - ≡-normalise-constant {a} {b} p q with a ≟ b - ... | true because _ = refl - ... | false because [¬p] = ⊥-elim (invert [¬p] p) + ≡-normalise {x} {y} x≡y = recompute (x ≟ y) x≡y + + ≡-normalise-constant : (p q : x ≡ y) → ≡-normalise p ≡ ≡-normalise q + ≡-normalise-constant {x = x} {y = y} = recompute-irr (x ≟ y) ≡-irrelevant : UIP A ≡-irrelevant = Constant⇒UIP.≡-irrelevant ≡-normalise ≡-normalise-constant diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda index 6b5fe5c120..698fafc879 100644 --- a/src/Relation/Nullary.agda +++ b/src/Relation/Nullary.agda @@ -25,7 +25,7 @@ private open import Relation.Nullary.Recomputable public using (Recomputable) open import Relation.Nullary.Negation.Core public -open import Relation.Nullary.Reflects public hiding (recompute) +open import Relation.Nullary.Reflects public hiding (recompute; recompute-irr) open import Relation.Nullary.Decidable.Core public ------------------------------------------------------------------------ diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda index 24037b6dc2..0e4d487b1b 100644 --- a/src/Relation/Nullary/Decidable/Core.agda +++ b/src/Relation/Nullary/Decidable/Core.agda @@ -74,8 +74,8 @@ module _ {A : Set a} where recompute : Dec A → Recomputable A recompute = Reflects.recompute ∘ proof -recompute-irr : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q -recompute-irr = Reflects.recompute-irr ∘ proof +recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q +recompute-constant = Reflects.recompute-constant ∘ proof ------------------------------------------------------------------------ -- Interaction with negation, sum, product etc. diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda index ad244bdc51..830b9d780c 100644 --- a/src/Relation/Nullary/Reflects.agda +++ b/src/Relation/Nullary/Reflects.agda @@ -61,8 +61,8 @@ recompute : ∀ {b} → Reflects A b → Recomputable A recompute (ofʸ a) _ = a recompute (ofⁿ ¬a) a = contradiction-irr a ¬a -recompute-irr : ∀ {b} (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q -recompute-irr r p q = refl +recompute-constant : ∀ {b} (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q +recompute-constant r p q = refl ------------------------------------------------------------------------ -- Interaction with negation, product, sums etc.