[ fix #645 ] Irrelevant Data.Empty

CHANGELOG.md

@@ -90,7 +90,6 @@ Non-backwards compatible changes
   So `[a-zA-Z]+.agdai?` run on "the path _build/Main.agdai corresponds to"
   will return "Main.agdai" when it used to be happy to just return "n.agda".
 
-
 ### Refactoring of algebraic lattice hierarchy
 
 * In order to improve modularity and consistency with `Relation.Binary.Lattice`,
@@ -386,6 +385,31 @@ Non-backwards compatible changes
   * `IsSemiringWithoutAnnihilatingZero*` and `isSemiringWithoutAnnihilatingZero*`
   * `IsRing*` and `isRing*`
 
+### Proof-irrelevant empty type
+
+* The definition of ⊥ has been changed to
+  ```agda
+  private
+    data Empty : Set where
+
+  ⊥ : Set
+  ⊥ = Irrelevant Empty
+  ```
+  in order to make ⊥ proof irrelevant. Any two proofs of `⊥` or of a negated
+  statements are now *judgementally* equal to each other.
+
+* Consequently we have modified the following definitions:
+  + In `Relation.Nullary.Decidable.Core`, the type of `dec-no` has changed
+    ```agda
+    dec-no : (p? : Dec P) → ¬ P → ∃ λ ¬p′ → p? ≡ no ¬p′
+      ↦ dec-no : (p? : Dec P) (¬p : ¬ P) → p? ≡ no ¬p
+    ```
+  + In `Relation.Binary.PropositionalEquality`, the type of `≢-≟-identity` has changed
+    ```agda
+    ≢-≟-identity : x ≢ y → ∃ λ ¬eq → x ≟ y ≡ no ¬eq
+      ↦ ≢-≟-identity : (x≢y : x ≢ y) → x ≟ y ≡ no x≢y
+    ```
+
 ### Other
 
 * The first two arguments of `m≡n⇒m-n≡0` (now `i≡j⇒i-j≡0`) in `Data.Integer.Base`
@@ -602,7 +626,7 @@ Deprecated names
   *-monoˡ-≤-neg    ↦  *-monoˡ-≤-nonPos
   *-cancelˡ-<-neg  ↦  *-cancelˡ-<-nonPos
   *-cancelʳ-<-neg  ↦  *-cancelʳ-<-nonPos
-  
+
   ^-semigroup-morphism ↦ ^-isMagmaHomomorphism
   ^-monoid-morphism    ↦ ^-isMonoidHomomorphism
   ```
@@ -709,6 +733,11 @@ Deprecated names
   invPreorder   ↦ converse-preorder
   ```
 
+### Renamed Data.Erased to Data.Irrelevant
+
+* This fixes the fact we had picked the wrong name originally. The erased modality
+  corresponds to @0 whereas the irrelevance one corresponds to `.`.
+
 New modules
 -----------
 
@@ -1021,7 +1050,7 @@ Other minor changes
   combine-injective  : combine i j ≡ combine k l → i ≡ k × j ≡ l
   combine-surjective : ∀ i → ∃₂ λ j k → combine j k ≡ i
   combine-monoˡ-<    :  i < j → combine i k < combine j l
-  
+
   lower₁-injective   : lower₁ i n≢i ≡ lower₁ j n≢j → i ≡ j
 
   i<1+i              : i < suc i
@@ -1065,7 +1094,7 @@ Other minor changes
   derunᵇ       : (A → A → Bool) → List A → List A
   deduplicateᵇ : (A → A → Bool) → List A → List A
   ```
-  
+
 * Added new proofs in `Data.List.Relation.Binary.Lex.Strict`:
   ```agda
   xs≮[] : ¬ xs < []
@@ -1245,9 +1274,9 @@ Other minor changes
 * Added new functions in `Data.String.Base`:
   ```agda
   wordsByᵇ : (Char → Bool) → String → List String
-  linesByᵇ : (Char → Bool) → String → List String 
+  linesByᵇ : (Char → Bool) → String → List String
   ```
-  
+
 * Added new proofs in `Data.String.Properties`:
   ```
   ≤-isDecTotalOrder-≈ : IsDecTotalOrder _≈_ _≤_
@@ -1488,6 +1517,9 @@ Other minor changes
   ≐′-trans : Trans _≐′_ _≐′_ _≐′_
   ≐⇒≐′ : _≐_ ⇒ _≐′_
   ≐′⇒≐ : _≐′_ ⇒ _≐_
+
+  U-irrelevant : Irrelevant {A = A} U
+  ∁-irrelevant : (P : Pred A ℓ) → Irrelevant (∁ P)
   ```
 
 * Generalised proofs in `Relation.Unary.Properties`:
@@ -1505,7 +1537,7 @@ Other minor changes
   ```
   record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   ```
-  
+
 * Added new definitions in `Relation.Binary.Structures`:
   ```
   record IsApartnessRelation (_#_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where

src/Data/Empty.agda

@@ -1,21 +1,34 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Empty type
+-- Empty type, judgementally proof irrelevant
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
 module Data.Empty where
 
+open import Data.Irrelevant using (Irrelevant)
+
 ------------------------------------------------------------------------
 -- Definition
 
 -- Note that by default the empty type is not universe polymorphic as it
 -- often results in unsolved metas. See `Data.Empty.Polymorphic` for a
 -- universe polymorphic variant.
 
-data ⊥ : Set where
+private
+  data Empty : Set where
+
+-- ⊥ is defined via Data.Irrelevant (a record with a single irrelevant field)
+-- so that Agda can judgementally declare that all proofs of ⊥ are equal
+-- to each other. In particular this means that all functions returning a
+-- proof of ⊥ are equal.
+
+⊥ : Set
+⊥ = Irrelevant Empty
+
+{-# DISPLAY Irrelevant Empty = ⊥ #-}
 
 ------------------------------------------------------------------------
 -- Functions

src/Data/Erased.agda

@@ -1,53 +1,21 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Wrapper for the erased modality
---
--- This allows us to store erased proofs in a record and use projections
--- to manipulate them without having to turn on the unsafe option
--- --irrelevant-projections.
+-- This module is DEPRECATED.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
 module Data.Erased where
 
-open import Level using (Level)
-
-private
-  variable
-    a b c : Level
-    A : Set a
-    B : Set b
-    C : Set c
-
-------------------------------------------------------------------------
--- Type
-
-record Erased (A : Set a) : Set a where
-  constructor [_]
-  field .erased : A
-open Erased public
-
-------------------------------------------------------------------------
--- Algebraic structure: Functor, Appplicative and Monad-like
-
-map : (A → B) → Erased A → Erased B
-map f [ a ] = [ f a ]
-
-pure : A → Erased A
-pure x = [ x ]
-
-infixl 4 _<*>_
-_<*>_ : Erased (A → B) → Erased A → Erased B
-[ f ] <*> [ a ] = [ f a ]
-
-infixl 1 _>>=_
-_>>=_ : Erased A → (.A → Erased B) → Erased B
-[ a ] >>= f = f a
-
-------------------------------------------------------------------------
--- Other functions
-
-zipWith : (A → B → C) → Erased A → Erased B → Erased C
-zipWith f a b = ⦇ f a b ⦈
+{-# WARNING_ON_IMPORT
+"Data.Erased was deprecated in v2.0.
+Use Data.Irrelevant instead."
+#-}
+
+open import Data.Irrelevant public
+  using ([_]; map; pure; _<*>_; _>>=_; zipWith)
+  renaming
+  ( Irrelevant to Erased
+  ; irrelevant to erased
+  )

src/Data/Fin/Permutation.agda

@@ -211,8 +211,10 @@ insert {m} {n} i j π = permutation to from record
   left-inverse-of : ∀ k → from (to k) ≡ k
   left-inverse-of k with i ≟ k
   ... | yes i≡k rewrite proj₂ (dec-yes (j ≟ j) refl) = i≡k
-  ... | no  i≢k with dec-no (j ≟ punchIn j (π ⟨$⟩ʳ punchOut i≢k)) (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)
-  ... | j≢punchInⱼπʳpunchOuti≢k , p rewrite p = begin
+  ... | no  i≢k
+    with j≢punchInⱼπʳpunchOuti≢k ← punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym
+    rewrite dec-no (j ≟ punchIn j (π ⟨$⟩ʳ punchOut i≢k)) j≢punchInⱼπʳpunchOuti≢k
+    = begin
     punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k)                    ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-cong j refl) ⟩
     punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-punchIn j) ⟩
     punchIn i (π ⟨$⟩ˡ (π ⟨$⟩ʳ punchOut i≢k))                              ≡⟨ cong (punchIn i) (inverseˡ π) ⟩
@@ -222,8 +224,10 @@ insert {m} {n} i j π = permutation to from record
   right-inverse-of : ∀ k → to (from k) ≡ k
   right-inverse-of k with j ≟ k
   ... | yes j≡k rewrite proj₂ (dec-yes (i ≟ i) refl) = j≡k
-  ... | no  j≢k with dec-no (i ≟ punchIn i (π ⟨$⟩ˡ punchOut j≢k)) (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)
-  ... | i≢punchInᵢπˡpunchOutj≢k , p rewrite p = begin
+  ... | no  j≢k
+    with i≢punchInᵢπˡpunchOutj≢k ← punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym
+    rewrite dec-no (i ≟ punchIn i (π ⟨$⟩ˡ punchOut j≢k)) i≢punchInᵢπˡpunchOutj≢k
+    = begin
     punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k)                    ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩
     punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩
     punchIn j (π ⟨$⟩ʳ (π ⟨$⟩ˡ punchOut j≢k))                              ≡⟨ cong (punchIn j) (inverseʳ π) ⟩

src/Data/Irrelevant.agda

@@ -0,0 +1,54 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Wrapper for the proof irrelevance modality
+--
+-- This allows us to store proof irrelevant witnesses in a record and
+-- use projections to manipulate them without having to turn on the
+-- unsafe option --irrelevant-projections.
+-- Cf. Data.Refinement for a use case
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Irrelevant where
+
+open import Level using (Level)
+
+private
+  variable
+    a b c : Level
+    A : Set a
+    B : Set b
+    C : Set c
+
+------------------------------------------------------------------------
+-- Type
+
+record Irrelevant (A : Set a) : Set a where
+  constructor [_]
+  field .irrelevant : A
+open Irrelevant public
+
+------------------------------------------------------------------------
+-- Algebraic structure: Functor, Appplicative and Monad-like
+
+map : (A → B) → Irrelevant A → Irrelevant B
+map f [ a ] = [ f a ]
+
+pure : A → Irrelevant A
+pure x = [ x ]
+
+infixl 4 _<*>_
+_<*>_ : Irrelevant (A → B) → Irrelevant A → Irrelevant B
+[ f ] <*> [ a ] = [ f a ]
+
+infixl 1 _>>=_
+_>>=_ : Irrelevant A → (.A → Irrelevant B) → Irrelevant B
+[ a ] >>= f = f a
+
+------------------------------------------------------------------------
+-- Other functions
+
+zipWith : (A → B → C) → Irrelevant A → Irrelevant B → Irrelevant C
+zipWith f a b = ⦇ f a b ⦈

src/Data/Refinement.agda

@@ -1,17 +1,17 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Refinement type: a value together with an erased proof.
+-- Refinement type: a value together with a proof irrelevant witness.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
 module Data.Refinement where
 
 open import Level
-open import Data.Erased as Erased using (Erased)
+open import Data.Irrelevant as Irrelevant using (Irrelevant)
 open import Function.Base
-open import Relation.Unary
+open import Relation.Unary using (IUniversal; _⇒_; _⊢_)
 
 private
   variable
@@ -22,7 +22,7 @@ private
 record Refinement {a p} (A : Set a) (P : A → Set p) : Set (a ⊔ p) where
   constructor _,_
   field value : A
-        proof : Erased (P value)
+        proof : Irrelevant (P value)
 open Refinement public
 
 -- The syntax declaration below is meant to mimick set comprehension.
@@ -37,7 +37,7 @@ module _ {P : A → Set p} {Q : B → Set q} where
 
   map : (f : A → B) → ∀[ P ⇒ f ⊢ Q ] →
         [ a ∈ A ∣ P a ] → [ b ∈ B ∣ Q b ]
-  map f prf (a , p) = f a , Erased.map prf p
+  map f prf (a , p) = f a , Irrelevant.map prf p
 
 module _ {P : A → Set p} {Q : A → Set q} where
 

src/Relation/Binary/PropositionalEquality.agda

@@ -113,10 +113,10 @@ cong-≡id {f = f} {x} f≡id =
   f≡id (f x)                                     ∎
   where open ≡-Reasoning; fx≡x = f≡id x; f²x≡x = f≡id (f x)
 
-module _ (_≟_ : Decidable {A = A} _≡_) {x y : A} where
+module _ (_≟_ : DecidableEquality A) {x y : A} where
 
   ≡-≟-identity : (eq : x ≡ y) → x ≟ y ≡ yes eq
   ≡-≟-identity eq = dec-yes-irr (x ≟ y) (Decidable⇒UIP.≡-irrelevant _≟_) eq
 
-  ≢-≟-identity : x ≢ y → ∃ λ ¬eq → x ≟ y ≡ no ¬eq
-  ≢-≟-identity ¬eq = dec-no (x ≟ y) ¬eq
+  ≢-≟-identity : (x≢y : x ≢ y) → x ≟ y ≡ no x≢y
+  ≢-≟-identity = dec-no (x ≟ y)

src/Relation/Nullary/Decidable/Core.agda

@@ -113,9 +113,9 @@ dec-yes : (p? : Dec P) → P → ∃ λ p′ → p? ≡ yes p′
 dec-yes p? p with dec-true p? p
 dec-yes (yes p′) p | refl = p′ , refl
 
-dec-no : (p? : Dec P) → ¬ P → ∃ λ ¬p′ → p? ≡ no ¬p′
+dec-no : (p? : Dec P) (¬p : ¬ P) → p? ≡ no ¬p
 dec-no p? ¬p with dec-false p? ¬p
-dec-no (no ¬p′) ¬p | refl = ¬p′ , refl
+dec-no (no _) _ | refl = refl
 
 dec-yes-irr : (p? : Dec P) → Irrelevant P → (p : P) → p? ≡ yes p
 dec-yes-irr p? irr p with dec-yes p? p

src/Relation/Unary/Properties.agda

@@ -8,12 +8,14 @@
 
 module Relation.Unary.Properties where
 
+open import Agda.Builtin.Equality using (refl)
+
 open import Data.Product as Product using (_×_; _,_; swap; proj₁; zip′)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Unit.Base using (tt)
 open import Level
 open import Relation.Binary.Core as Binary
-open import Relation.Binary.Definitions hiding (Decidable; Universal)
+open import Relation.Binary.Definitions hiding (Decidable; Universal; Irrelevant)
 open import Relation.Unary
 open import Relation.Nullary using (yes; no)
 open import Relation.Nullary.Product using (_×-dec_)
@@ -227,3 +229,12 @@ _⊎?_ P? Q? (inj₂ b) = Q? b
 
 _~? : {P : Pred (A × B) ℓ} → Decidable P → Decidable (P ~)
 _~? P? = P? ∘ swap
+
+----------------------------------------------------------------------
+-- Irrelevant properties
+
+U-irrelevant : Irrelevant {A = A} U
+U-irrelevant a b = refl
+
+∁-irrelevant : (P : Pred A ℓ) → Irrelevant (∁ P)
+∁-irrelevant P a b = refl