Start design doc

CHANGELOG.md

@@ -572,3 +572,5 @@ Other minor additions
   toSum   :  Refl _~_ a b   → a ≡ b ⊎ a ~ b
   ⊎⇔Refl  : (a ≡ b ⊎ a ~ b) ⇔ Refl _~_ a b
   ```
+
+* Started documenting design decisions about the library in `DESIGN.md`

DESIGN.md

@@ -0,0 +1,12 @@
+Library Design
+==============
+
+Documents library design decisions, big and small.
+
+Smaller Design Decisions
+------------------------
+
+- `⊥` in `Data.Empty` and `⊤` in `Data.Unit` are not `Level`-polymorphic as that
+  tends to lead to unsolved metas (see discussion at issue #312).  For that purpose,
+  there are now level-polymorphic version in `Data.Empty.Polymorphic` and
+  `Data.Unit.Polymorphic` respectively.

src/Data/Unit.agda

@@ -42,22 +42,26 @@ decSetoid = Data.Unit.Properties.≡-decSetoid
 "Warning: decSetoid was deprecated in v1.1.
 Please use ≡-decSetoid from Data.Unit.Properties instead."
 #-}
-total = Data.Unit.Properties.≤-total
+
+-- Version 1.2
+total = Data.Unit.Properties.≡-total
 {-# WARNING_ON_USAGE total
-"Warning: total was deprecated in v1.1.
-Please use ≤-total from Data.Unit.Properties instead."
+"Warning: total was deprecated in v1.2.
+Please use Data.Unit.Properties.≡-total instead"
 #-}
-poset = Data.Unit.Properties.≤-poset
+poset = Data.Unit.Properties.≡-poset
 {-# WARNING_ON_USAGE poset
-"Warning: poset was deprecated in v1.1.
-Please use ≤-poset from Data.Unit.Properties instead."
+"Warning: poset was deprecated in v1.2.
+Please use ≡-poset from Data.Unit.Properties instead."
 #-}
-decTotalOrder = Data.Unit.Properties.≤-decTotalOrder
+decTotalOrder = Data.Unit.Properties.≡-decTotalOrder
 {-# WARNING_ON_USAGE decTotalOrder
-"Warning: decTotalOrder was deprecated in v1.1.
-Please use ≤-decTotalOrder from Data.Unit.Properties instead."
+"Warning: decTotalOrder was deprecated in v1.2.
+Please use ≡-decTotalOrder from Data.Unit.Properties instead."
 #-}
 preorder = PropEq.preorder ⊤
 {-# WARNING_ON_USAGE decTotalOrder
-"Warning: preorder was deprecated in v1.1."
+"Warning: preorder was deprecated in v1.2."
 #-}
+
+-- Version 1.2

src/Data/Unit/Base.agda

@@ -6,17 +6,30 @@
 
 {-# OPTIONS --without-K --safe #-}
 
+open import Agda.Builtin.Equality using (_≡_)
+
 module Data.Unit.Base where
 
 ------------------------------------------------------------------------
 -- A unit type defined as a record type
 
 open import Agda.Builtin.Unit public
   using (⊤; tt)
-
 -- Note that the name of this type is "\top", not T.
 
+
 ------------------------------------------------------------------------
--- An ordering relation over the unit type
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 1.2
+
+_≤_ : (x y : ⊤) → Set
+_≤_ = _≡_
 
-record _≤_ (x y : ⊤) : Set where
+{-# WARNING_ON_USAGE _≤_
+"Warning: _≤_ was deprecated in v1.2.
+Please use _≡_ from Relation.Binary.PropositionalEquality instead."
+#-}

src/Data/Unit/Polymorphic.agda

@@ -14,5 +14,4 @@ open import Data.Unit.Polymorphic.Base public
 ------------------------------------------------------------------------
 -- Re-export query operations
 
-open import Data.Unit.Polymorphic.Properties public
-  using (_≟_; _≤?_)
+open import Data.Unit.Polymorphic.Properties public using (_≟_)

src/Data/Unit/Polymorphic/Base.agda

@@ -15,8 +15,3 @@ open import Level
 
 record ⊤ {ℓ : Level} : Set ℓ where
   constructor tt
-
-------------------------------------------------------------------------
--- An ordering relation over the unit type
-
-record _≤_ {ℓ ℓ′ e : Level} (x : ⊤ {ℓ}) (y : ⊤ {ℓ′}) : Set e where

src/Data/Unit/Polymorphic/Properties.agda

@@ -11,14 +11,14 @@ module Data.Unit.Polymorphic.Properties where
 
 open import Level
 open import Data.Sum using (inj₁)
-open import Data.Unit.Polymorphic.Base using (⊤; tt; _≤_)
+open import Data.Unit.Polymorphic.Base using (⊤; tt)
 open import Relation.Nullary
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality
 
 private
   variable
-    ℓ ℓ′ a b e : Level
+    ℓ : Level
 
 ------------------------------------------------------------------------
 -- Decidable Equality and Ordering
@@ -28,11 +28,6 @@ infix 4 _≟_
 _≟_ : {ℓ : Level} → Decidable {A = ⊤ {ℓ}} _≡_
 _ ≟ _ = yes refl
 
-infix 4 _≤?_
-
-_≤?_ : {a b ℓ : Level} → Decidable {a} {_} {b} {ℓ = ℓ}  _≤_
-_ ≤? _ = yes _
-
 ------------------------------------------------------------------------
 -- Setoid
 
@@ -43,59 +38,44 @@ _ ≤? _ = yes _
 ≡-decSetoid = decSetoid _≟_
 
 ------------------------------------------------------------------------
--- _≤_
-
 -- Relational properties
 
-≤-reflexive : _≡_ {a} ⇒ (_≤_ {e = e})
-≤-reflexive _ = _
-
-≤-trans : Transitive (_≤_ {ℓ} {e = e})
-≤-trans _ _ = _
-
-≤-antisym : Antisymmetric _≡_ (_≤_ {ℓ} {e = e})
-≤-antisym  _ _ = refl
-
-≤-total : Total (_≤_ {ℓ} {e = e})
-≤-total _ _ = inj₁ _
-
-
 -- Structures
 
-≤-isPreorder : IsPreorder _≡_ (_≤_ {ℓ} {e = e})
-≤-isPreorder = record
+≡-isPreorder : IsPreorder {ℓ} {_} {⊤ {ℓ}} _≡_ _≡_
+≡-isPreorder = record
   { isEquivalence = isEquivalence
-  ; reflexive     = ≤-reflexive
-  ; trans         = ≤-trans
+  ; reflexive     = λ x → x
+  ; trans         = trans
   }
 
-≤-isPartialOrder : IsPartialOrder _≡_ (_≤_ {ℓ} {e = e})
-≤-isPartialOrder = record
-  { isPreorder = ≤-isPreorder
-  ; antisym    = ≤-antisym
+≡-isPartialOrder : IsPartialOrder {ℓ} _≡_ _≡_
+≡-isPartialOrder = record
+  { isPreorder = ≡-isPreorder
+  ; antisym    = λ p _ → p
   }
 
-≤-isTotalOrder : IsTotalOrder _≡_ (_≤_ {ℓ} {e = e})
-≤-isTotalOrder = record
-  { isPartialOrder = ≤-isPartialOrder
-  ; total          = ≤-total
+≡-isTotalOrder : IsTotalOrder {ℓ} _≡_ _≡_
+≡-isTotalOrder = record
+  { isPartialOrder = ≡-isPartialOrder
+  ; total          = λ _ _ → inj₁ refl
   }
 
-≤-isDecTotalOrder : IsDecTotalOrder _≡_ (_≤_ {ℓ} {e = e})
-≤-isDecTotalOrder = record
-  { isTotalOrder = ≤-isTotalOrder
+≡-isDecTotalOrder : IsDecTotalOrder {ℓ} _≡_ _≡_
+≡-isDecTotalOrder = record
+  { isTotalOrder = ≡-isTotalOrder
   ; _≟_          = _≟_
-  ; _≤?_         = _≤?_
+  ; _≤?_         = _≟_
   }
 
 -- Bundles
 
-≤-poset : Poset ℓ ℓ b
-≤-poset = record
-  { isPartialOrder = ≤-isPartialOrder
+≡-poset : Poset ℓ ℓ ℓ
+≡-poset = record
+  { isPartialOrder = ≡-isPartialOrder
   }
 
-≤-decTotalOrder : DecTotalOrder ℓ ℓ b
-≤-decTotalOrder = record
-  { isDecTotalOrder = ≤-isDecTotalOrder
+≡-decTotalOrder : DecTotalOrder ℓ ℓ ℓ
+≡-decTotalOrder = record
+  { isDecTotalOrder = ≡-isDecTotalOrder
   }

src/Data/Unit/Properties.agda

@@ -30,63 +30,119 @@ _ ≟ _ = yes refl
 ≡-decSetoid = decSetoid _≟_
 
 ------------------------------------------------------------------------
--- _≤_
 
 -- Relational properties
+-- These are all deprecated as _≤_ is _≡_ now
 
-≤-reflexive : _≡_ ⇒ _≤_
-≤-reflexive _ = _
-
-≤-trans : Transitive _≤_
-≤-trans _ _ = _
-
-≤-antisym : Antisymmetric _≡_ _≤_
-≤-antisym  _ _ = refl
-
-≤-total : Total _≤_
-≤-total _ _ = inj₁ _
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 1.2
+
+≤-reflexive : _⇒_ {A = ⊤} _≡_ _≡_
+≤-reflexive p = p
+{-# WARNING_ON_USAGE ≤-reflexive
+"Warning: ≤-reflexive was deprecated in v1.2.
+Please use id from Function instead."
+#-}
+
+≤-trans : Transitive {A = ⊤} _≡_
+≤-trans = trans
+{-# WARNING_ON_USAGE ≤-trans
+"Warning: ≤-trans was deprecated in v1.2.
+Please use trans from Relation.Binary.PropositionalEquality instead."
+#-}
+
+≤-antisym : Antisymmetric {A = ⊤} _≡_ _≡_
+≤-antisym p _ = p
+{-# WARNING_ON_USAGE ≤-antisym
+"Warning: ≤-antisym was deprecated in v1.2."
+#-}
+
+≡-total : Total {A = ⊤} _≡_
+≡-total _ _ = inj₁ refl
+≤-total = ≡-total
+{-# WARNING_ON_USAGE ≤-total
+"Warning: ≤-total was deprecated in v1.2."
+#-}
 
 infix 4 _≤?_
 
-_≤?_ : Decidable _≤_
-_ ≤? _ = yes _
+_≤?_ = _≟_
+{-# WARNING_ON_USAGE _≤?_
+"Warning: _≤_ was deprecated in v1.2.
+Please use _≟_ from Relation.Binary.PropositionalEquality instead."
+#-}
 
 -- Structures
 
-≤-isPreorder : IsPreorder _≡_ _≤_
-≤-isPreorder = record
+≡-isPreorder : IsPreorder {A = ⊤} _≡_ _≡_
+≡-isPreorder = record
   { isEquivalence = isEquivalence
-  ; reflexive     = ≤-reflexive
-  ; trans         = ≤-trans
+  ; reflexive     = λ x → x
+  ; trans         = trans
   }
-
-≤-isPartialOrder : IsPartialOrder _≡_ _≤_
-≤-isPartialOrder = record
-  { isPreorder = ≤-isPreorder
-  ; antisym    = ≤-antisym
+≤-isPreorder = ≡-isPreorder
+{-# WARNING_ON_USAGE ≤-isPreorder
+"Warning: ≤-isPreorder was deprecated in v1.2.
+Please use ≡-isPreorder instead."
+#-}
+
+≡-isPartialOrder : IsPartialOrder _≡_ _≡_
+≡-isPartialOrder = record
+  { isPreorder = ≡-isPreorder
+  ; antisym    = λ p _ → p
   }
-
-≤-isTotalOrder : IsTotalOrder _≡_ _≤_
-≤-isTotalOrder = record
-  { isPartialOrder = ≤-isPartialOrder
-  ; total          = ≤-total
+≤-isPartialOrder = ≡-isPartialOrder
+{-# WARNING_ON_USAGE ≤-isPartialOrder
+"Warning: ≤-isPartialOrder was deprecated in v1.2.
+Please use ≡-isPartialOrder instead."
+#-}
+
+≡-isTotalOrder : IsTotalOrder _≡_ _≡_
+≡-isTotalOrder = record
+  { isPartialOrder = ≡-isPartialOrder
+  ; total          = λ _ _ → inj₁ refl
   }
-
-≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
-≤-isDecTotalOrder = record
-  { isTotalOrder = ≤-isTotalOrder
+≤-isTotalOrder = ≡-isTotalOrder
+{-# WARNING_ON_USAGE ≤-isTotalOrder
+"Warning: ≤-isTotalOrder was deprecated in v1.2.
+Please use ≡-isTotalOrder instead."
+#-}
+
+≡-isDecTotalOrder : IsDecTotalOrder _≡_ _≡_
+≡-isDecTotalOrder = record
+  { isTotalOrder = ≡-isTotalOrder
   ; _≟_          = _≟_
-  ; _≤?_         = _≤?_
+  ; _≤?_         = _≟_
   }
+≤-isDecTotalOrder = ≡-isDecTotalOrder
+{-# WARNING_ON_USAGE ≤-isDecTotalOrder
+"Warning: ≤-isDecTotalOrder was deprecated in v1.2.
+Please use ≡-isDecTotalOrder instead."
+#-}
 
 -- Packages
 
-≤-poset : Poset 0ℓ 0ℓ 0ℓ
-≤-poset = record
-  { isPartialOrder = ≤-isPartialOrder
+≡-poset : Poset 0ℓ 0ℓ 0ℓ
+≡-poset = record
+  { isPartialOrder = ≡-isPartialOrder
   }
-
-≤-decTotalOrder : DecTotalOrder 0ℓ 0ℓ 0ℓ
-≤-decTotalOrder = record
-  { isDecTotalOrder = ≤-isDecTotalOrder
+≤-poset = ≡-poset
+{-# WARNING_ON_USAGE ≤-poset
+"Warning: ≤-poset was deprecated in v1.2.
+Please use ≡-poset instead."
+#-}
+
+≡-decTotalOrder : DecTotalOrder 0ℓ 0ℓ 0ℓ
+≡-decTotalOrder = record
+  { isDecTotalOrder = ≡-isDecTotalOrder
   }
+≤-decTotalOrder = ≡-decTotalOrder
+{-# WARNING_ON_USAGE ≤-decTotalOrder
+"Warning: ≤-decTotalOrder was deprecated in v1.2.
+Please use ≡-decTotalOrder instead."
+#-}