Polymorphic unit and empty rethink (#1204)

Author: JacquesCarette

CHANGELOG.md

@@ -21,6 +21,12 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
+* `Data.Empty.Polymorphic` and `Data.Unit.Polymorphic` were rewritten
+  to explicitly use `Lift` rather that defining new types. This means
+  that these are now compatible with `⊥` and `⊤` from the rest of the
+  library. This allowed them to be used in the rest of library where
+  explicit `Lift` was used.
+
 Deprecated modules
 ------------------
 
@@ -44,8 +50,8 @@ Deprecated names
   * `Relation.Binary.Construct.StrictToNonStrict.decidable'` ↦ `Relation.Binary.Construct.StrictToNonStrict.decidable′`
 
 
-Other major additions
----------------------
+New modules
+-----------
 
 * Instance modules:
   ```agda
@@ -93,6 +99,11 @@ Other major additions
   Data.Nat.Binary.Subtraction
   ```
 
+* Indexed nullary relations/sets:
+  ```
+  Relation.Nullary.Indexed
+  ```
+ 
 Other major changes
 -------------------
 
@@ -300,7 +311,6 @@ Other minor additions
   nonPositive : p ≤ 0ℚᵘ → NonPositive p
   nonNegative : p ≥ 0ℚᵘ → NonNegative p
   ```
-
 * Added new operator to `Relation.Binary`:
   ```agda
   _⇔_ : REL A B ℓ₁ → REL A B ℓ₂ → Set _

src/Category/Applicative.agda

@@ -26,7 +26,7 @@ module RawApplicative {F : Set f → Set f}
                       (app : RawApplicative F) where
   open RawIApplicative app public
 
-RawApplicativeZero : (Set f → Set f) → Set _
+RawApplicativeZero : (Set f → Set f) → Set (suc f)
 RawApplicativeZero F = RawIApplicativeZero {I = ⊤} (λ _ _ → F)
 
 module RawApplicativeZero {F : Set f → Set f}

src/Category/Monad/Reader.agda

@@ -102,7 +102,7 @@ ReaderTIMonadReader Mon = record
 ------------------------------------------------------------------------
 -- Ordinary reader monads
 
-RawMonadReader : (M : Set (r ⊔ a) → Set (r ⊔ a)) → Set _
+RawMonadReader : (M : Set (r ⊔ a) → Set (r ⊔ a)) → Set (suc (r ⊔ a))
 RawMonadReader M = RawIMonadReader {I = ⊤} (λ _ _ → M)
 
 module RawMonadReader {M} (Mon : RawMonadReader M) where

src/Category/Monad/State.agda

@@ -105,7 +105,7 @@ StateTIMonadState S Mon = record
 ------------------------------------------------------------------------
 -- Ordinary state monads
 
-RawMonadState : Set f → (Set f → Set f) → Set _
+RawMonadState : Set f → (Set f → Set f) → Set (suc f)
 RawMonadState S M = RawIMonadState {I = ⊤} (λ _ → S) (λ _ _ → M)
 
 module RawMonadState {S : Set f} {M : Set f → Set f}

src/Data/Container/Combinator.agda

@@ -8,11 +8,11 @@
 
 module Data.Container.Combinator where
 
-open import Level using (Level; _⊔_; Lift)
-open import Data.Empty using (⊥)
+open import Level using (Level; _⊔_)
+open import Data.Empty.Polymorphic using (⊥)
 open import Data.Product as P using (_,_; proj₁; proj₂; ∃)
 open import Data.Sum.Base as S using ([_,_]′)
-open import Data.Unit.Base using (⊤)
+open import Data.Unit.Polymorphic.Base using (⊤)
 import Function as F
 
 open import Data.Container.Core
@@ -26,14 +26,14 @@ module _ {s p : Level} where
 -- Identity.
 
   id : Container s p
-  id .Shape    = Lift s ⊤
-  id .Position = F.const (Lift p ⊤)
+  id .Shape    = ⊤
+  id .Position = F.const ⊤
 
 -- Constant.
 
   const : Set s → Container s p
   const X .Shape    = X
-  const X .Position = F.const (Lift p ⊥)
+  const X .Position = F.const ⊥
 
 -- Composition.
 

src/Data/Container/Indexed/Combinator.agda

@@ -10,8 +10,8 @@ module Data.Container.Indexed.Combinator where
 
 open import Axiom.Extensionality.Propositional using (Extensionality)
 open import Data.Container.Indexed
-open import Data.Empty using (⊥; ⊥-elim)
-open import Data.Unit.Base using (⊤)
+open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
+open import Data.Unit.Polymorphic.Base using (⊤)
 open import Data.Product as Prod hiding (Σ) renaming (_×_ to _⟨×⟩_)
 open import Data.Sum renaming (_⊎_ to _⟨⊎⟩_)
 open import Function as F hiding (id; const) renaming (_∘_ to _⟨∘⟩_)
@@ -29,13 +29,13 @@ open import Relation.Binary.PropositionalEquality as P
 -- Identity.
 
 id : ∀ {o c r} {O : Set o} → Container O O c r
-id = F.const (Lift _ ⊤) ◃ (λ _ → Lift _ ⊤) / (λ {o} _ _ → o)
+id = F.const ⊤ ◃ F.const ⊤ / (λ {o} _ _ → o)
 
 -- Constant.
 
 const : ∀ {i o c r} {I : Set i} {O : Set o} →
         Pred O c → Container I O c r
-const X = X ◃ (λ _ → Lift _ ⊥) / λ _ → ⊥-elim ⟨∘⟩ lower
+const X = X ◃ F.const ⊥ / F.const ⊥-elim
 
 -- Duality.
 
@@ -165,10 +165,10 @@ module Constant (ext : ∀ {ℓ} → Extensionality ℓ ℓ) where
     to = proj₁
 
     from : X ⊆ ⟦ const X ⟧ Y
-    from = < F.id , F.const (⊥-elim ⟨∘⟩ lower) >
+    from = < F.id , F.const ⊥-elim >
 
     to∘from : _
-    to∘from xs = P.cong (proj₁ xs ,_) (ext (⊥-elim ⟨∘⟩ lower))
+    to∘from xs = P.cong (proj₁ xs ,_) (ext ⊥-elim)
 
 module Duality where
 

src/Data/Empty/Polymorphic.agda

@@ -8,9 +8,12 @@
 
 module Data.Empty.Polymorphic where
 
+import Data.Empty as Empty
 open import Level
 
-data ⊥ {ℓ : Level} : Set ℓ where
+⊥ : {ℓ : Level} → Set ℓ
+⊥ {ℓ} = Lift ℓ Empty.⊥
 
-⊥-elim : ∀ {w ℓ} {Whatever : Set w} → ⊥ {ℓ} → Whatever
+-- make ⊥-elim dependent too, as it does seem useful
+⊥-elim : ∀ {w ℓ} {Whatever : ⊥ {ℓ} → Set w} → (witness : ⊥ {ℓ}) → Whatever witness
 ⊥-elim ()

src/Data/List/Fresh.agda

@@ -13,9 +13,9 @@
 
 module Data.List.Fresh where
 
-open import Level using (Level; _⊔_; Lift)
+open import Level using (Level; _⊔_)
 open import Data.Bool.Base using (true; false)
-open import Data.Unit.Base
+open import Data.Unit.Polymorphic.Base using (⊤)
 open import Data.Product using (∃; _×_; _,_; -,_; proj₁; proj₂)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
@@ -57,7 +57,7 @@ module _ {a} (A : Set a) (R : Rel A r) where
   infixr 5 _∷#_
   pattern _∷#_ x xs = cons x xs _
 
-  fresh a []        = Lift _ ⊤
+  fresh a []        = ⊤
   fresh a (x ∷# xs) = R a x × fresh a xs
 
 -- Convenient notation for freshness making A and R implicit parameters

src/Data/List/Relation/Binary/BagAndSetEquality.agda

@@ -26,15 +26,14 @@ import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base as Sum hiding (map)
 open import Data.Sum.Properties hiding (map-cong)
 open import Data.Sum.Function.Propositional using (_⊎-cong_)
-open import Data.Unit
+open import Data.Unit.Polymorphic.Base
 open import Function.Base
 open import Function.Equality using (_⟨$⟩_)
 import Function.Equivalence as FE
 open import Function.Inverse as Inv using (_↔_; Inverse; inverse)
 open import Function.Related as Related
   using (↔⇒; ⌊_⌋; ⌊_⌋→; ⇒→; K-refl; SK-sym)
 open import Function.Related.TypeIsomorphisms
-open import Level using (Lift)
 open import Relation.Binary
 import Relation.Binary.Reasoning.Setoid as EqR
 import Relation.Binary.Reasoning.Preorder as PreorderReasoning
@@ -359,7 +358,7 @@ drop-cons {A = A} {x} {xs} {ys} x∷xs≈x∷ys =
     (∃ λ z → z ∈ xs)                   ↔⟨ Σ.cong K-refl (∈-index xs) ⟩
     (∃ λ z → ∃ λ i → z ≡ lookup xs i)  ↔⟨ ∃∃↔∃∃ _ ⟩
     (∃ λ i → ∃ λ z → z ≡ lookup xs i)  ↔⟨ Σ.cong K-refl (inverse _ (λ _ → _ , refl) (λ { (_ , refl) → refl }) (λ _ → refl)) ⟩
-    (Fin (length xs) × Lift _ ⊤)       ↔⟨ ×-identityʳ _ _ ⟩
+    (Fin (length xs) × ⊤)              ↔⟨ ×-identityʳ _ _ ⟩
     Fin (length xs)                    ∎
     where
     open Related.EquationalReasoning

src/Data/Nat/Induction.agda

@@ -12,10 +12,9 @@ open import Function
 open import Data.Nat.Base
 open import Data.Nat.Properties using (≤⇒≤′)
 open import Data.Product
-open import Data.Unit
+open import Data.Unit.Polymorphic
 open import Induction
 open import Induction.WellFounded as WF
-open import Level using (Lift)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Unary
 
@@ -28,7 +27,7 @@ open WF public using (Acc; acc)
 -- Ordinary induction
 
 Rec : ∀ ℓ → RecStruct ℕ ℓ ℓ
-Rec ℓ P zero    = Lift ℓ ⊤
+Rec ℓ P zero    = ⊤
 Rec ℓ P (suc n) = P n
 
 recBuilder : ∀ {ℓ} → RecursorBuilder (Rec ℓ)
@@ -42,7 +41,7 @@ rec = build recBuilder
 -- Complete induction
 
 CRec : ∀ ℓ → RecStruct ℕ ℓ ℓ
-CRec ℓ P zero    = Lift ℓ ⊤
+CRec ℓ P zero    = ⊤
 CRec ℓ P (suc n) = P n × CRec ℓ P n
 
 cRecBuilder : ∀ {ℓ} → RecursorBuilder (CRec ℓ)