knock-on, plus proof of UIP from agda#2149

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`

src/Axiom/UniquenessOfIdentityProofs.agda

@@ -8,23 +8,27 @@
 
 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
 --
 -- Uniqueness of Identity Proofs (UIP) states that all proofs of
 -- 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

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
 
 ------------------------------------------------------------------------

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.

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.