various updates

Prelude.agda

@@ -2,22 +2,30 @@ module Prelude where
 
 open import Function public
 
-open import Agda.Primitive public using (Level ; lzero ; lsuc ; _⊔_)
-open import Level public using (Lift ; lift ; lower)
-instance liftᴵ : ∀ {a ℓ} {A : Set a} → ⦃ A ⦄ → Lift ℓ A
-liftᴵ = lift it
-
 open import Agda.Builtin.FromNat public
 open import Agda.Builtin.FromNeg public
 open import Agda.Builtin.FromString public
 
+module Level where
+  open import Agda.Primitive public using (Level ; lzero ; lsuc ; _⊔_)
+  open import Level public using (Lift ; lift ; lower)
+  import Level.Literals as Lit
+
+  instance liftᴵ : ∀ {a ℓ} {A : Set a} → ⦃ A ⦄ → Lift ℓ A
+  liftᴵ = lift it
+
+  instance number : Number Level
+  number = Lit.Levelℕ
+open Level public using (Level ; lzero ; lsuc ; _⊔_)
+
+
 module ⊤ where
   open import Data.Unit public hiding (module ⊤)
   open import Data.Unit.Properties public
 open ⊤ public using (⊤ ; tt)
 
 module ⊥ where
-  open import Data.Empty public hiding (module ⊥ ; ⊥-elim)
+  open import Data.Empty public hiding (⊥-elim)
   open import Data.Empty.Irrelevant public
 open ⊥ public using (⊥ ; ⊥-elim)
 
@@ -33,10 +41,10 @@ module Fin where
   import Data.Fin hiding (module Fin)
   open Data.Fin public
   open import Data.Fin.Properties public
-  import Data.Fin.Literals as Lit
+  open import Data.Fin.Literals public renaming (number to number′)
 
   instance number : ∀ {n} → Number (Fin n)
-  number = Lit.number _
+  number = number′ $-
 open Fin public using (Fin ; zero ; suc ; #_)
 
 module Bool where
@@ -71,17 +79,25 @@ module Maybe where
 open Maybe public using (Maybe ; nothing ; just)
 
 module Rel where
-  open import Relation.Nullary public renaming (Irrelevant to Irrelevant₀)
+  open import Relation.Nullary public renaming
+    (Irrelevant to Irrelevant₀ ; Stable to Stable₀ ;
+     WeaklyDecidable to WeaklyDecidable₀)
   open import Relation.Nullary.Decidable public
   open import Relation.Unary public hiding (⌊_⌋)
     renaming (Irrelevant to Irrelevant₁ ; Recomputable to Recomputable₁ ;
-              Universal to Universal₁ ; Decidable to Decidable₁ ; _⇒_ to _⇒₁_)
+              Stable to Stable₁ ; WeaklyDecidable to WeaklyDecidable₁ ;
+              Universal to Universal₁ ; Decidable to Decidable₁ ; Empty to Empty₁ ;
+              _⇒_ to _⇒₁_)
   open import Relation.Binary public
     renaming (Irrelevant to Irrelevant₂ ; Recomputable to Recomputable₂ ;
-              Universal to Universal₂ ; Decidable to Decidable₂ ; _⇒_ to _⇒₂_)
+              Stable to Stable₂ ; WeaklyDecidable to WeaklyDecidable₂ ;
+              Universal to Universal₂ ; Decidable to Decidable₂ ; Empty to Empty₂ ;
+              _⇒_ to _⇒₂_)
 
   module _ where
-    private variable ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ ℓ₇ : Level ; A B C D E F G : Set _
+    private variable
+      ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ ℓ₇ : Level
+      A B C D E F G : Set _
 
     _Preserves₃_⟶_⟶_⟶_ :
       (A → B → C → D) → Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → Rel D ℓ₄ → Set _
@@ -138,39 +154,67 @@ module ≡ where
 open ≡ public using (_≡_ ; _≢_ ; refl) renaming (At to ≡-At)
 
 
-record Eq {a} (A : Set a) : Set a where
+module IsDecidable where
-  field _≟_ : Decidable₂ $ ≡-At A
+  record IsDecidable {a r} {A : Set a} (R : Rel A r) : Set (a ⊔ r) where
-open Eq ⦃ … ⦄ public
+    field dec : Decidable₂ R
+
+  open IsDecidable ⦃ … ⦄ public
+
+  private variable
+    a b : Level
+    A B : Set a
+    F : A → Set b
+    n : ℕ
+
+  Eq : Set a → Set _
+  Eq = IsDecidable ∘ ≡-At
+
+  _≟_ : ⦃ Eq A ⦄ → Decidable₂ (≡-At A)
+  _≟_ = dec
 
-module _ where
-  private variable a b : Level ; A : Set a ; B : Set b ; F : A → Set b ; n : ℕ
   instance
     eq-⊤ : Eq ⊤
-    eq-⊤ ._≟_ = ⊤._≟_
+    eq-⊤ .dec _ _ = yes refl
 
     eq-⊥ : Eq ⊥
-    eq-⊥ ._≟_ () ()
+    eq-⊥ .dec () ()
 
     eq-ℕ : Eq ℕ
-    eq-ℕ ._≟_ = ℕ._≟_
+    eq-ℕ .dec = ℕ._≟_
 
     eq-fin : Eq (Fin n)
-    eq-fin ._≟_ = Fin._≟_
+    eq-fin .dec = Fin._≟_
 
     eq-bool : Eq Bool
-    eq-bool ._≟_ = Bool._≟_
+    eq-bool .dec = Bool._≟_
 
     eq-⊎ : ⦃ Eq A ⦄ → ⦃ Eq B ⦄ → Eq (A ⊎ B)
-    eq-⊎ ._≟_ = ⊎.≡-dec _≟_ _≟_
+    eq-⊎ .dec = ⊎.≡-dec dec dec
 
     eq-prod : ⦃ Eq A ⦄ → ⦃ Rel.∀[ Eq ∘ F ] ⦄ → Eq (Σ A F)
-    eq-prod ._≟_ = Σ.≡-dec _≟_ _≟_
+    eq-prod .dec = Σ.≡-dec dec dec
 
     eq-maybe : ⦃ Eq A ⦄ → Eq (Maybe A)
-    eq-maybe ._≟_ = Maybe.≡-dec _≟_
+    eq-maybe .dec = Maybe.≡-dec dec
 
     eq-list : ⦃ Eq A ⦄ → Eq (List A)
-    eq-list ._≟_ = List.≡-dec _≟_
+    eq-list .dec = List.≡-dec dec
 
     eq-vec : ⦃ Eq A ⦄ → Eq (Vec A n)
-    eq-vec ._≟_ = Vec.≡-dec _≟_
+    eq-vec .dec = Vec.≡-dec dec
+open IsDecidable public
+  using (IsDecidable ; dec ; Eq ; _≟_)
+  hiding (module IsDecidable)
+
+
+module Uninhabited where
+  record Uninhabited {a} (A : Set a) : Set a where
+    field absurd′ : ¬ A
+  open Uninhabited ⦃ … ⦄
+
+  private variable
+    a b : Level
+    A B : Set a
+
+  absurd : ⦃ Uninhabited A ⦄ → A → B
+  absurd x with () ← absurd′ x