Add consistent deprecation warnings to old function hierarchy

CHANGELOG.md

@@ -1993,6 +1993,7 @@ New modules
   Function.Properties.Bijection
   Function.Properties.RightInverse
   Function.Properties.Surjection
+  Function.Construct.Constant
   ```
 
 * In order to improve modularity, the contents of `Relation.Binary.Lattice` has been

src/Data/Product/Function/Dependent/Setoid.agda

@@ -16,11 +16,10 @@ open import Data.Product.Relation.Binary.Pointwise.Dependent as Σ
 open import Level using (Level)
 open import Function
 open import Function.Consequences
-open import Function.Properties.Injection
-open import Function.Properties.Surjection
-open import Function.Properties.Equivalence
-open import Function.Properties.RightInverse
-import Function.Properties.Inverse as InverseProperties
+open import Function.Properties.Injection using (mkInjection)
+open import Function.Properties.Surjection using (mkSurjection; ↠⇒⇔)
+open import Function.Properties.Equivalence using (mkEquivalence; ⇔⇒⟶; ⇔⇒⟵)
+open import Function.Properties.RightInverse using (mkRightInverse)
 open import Relation.Binary.Core using (_=[_]⇒_)
 open import Relation.Binary.Bundles as B
 open import Relation.Binary.Indexed.Heterogeneous

src/Function/Bijection.agda

@@ -38,6 +38,10 @@ record Bijective {f₁ f₂ t₁ t₂}
 
   left-inverse-of : from LeftInverseOf to
   left-inverse-of x = injective (right-inverse-of (to ⟨$⟩ x))
+{-# WARNING_ON_USAGE Bijective
+"Warning: Bijective was deprecated in v2.0.
+Please use Function.(Structures.)IsBijection instead."
+#-}
 
 ------------------------------------------------------------------------
 -- The set of all bijections between two setoids.
@@ -74,6 +78,10 @@ record Bijection {f₁ f₂ t₁ t₂}
     }
 
   open LeftInverse left-inverse public using (to-from)
+{-# WARNING_ON_USAGE Bijection
+"Warning: Bijection was deprecated in v2.0.
+Please use Function.(Bundles.)Bijection instead."
+#-}
 
 ------------------------------------------------------------------------
 -- The set of all bijections between two sets (i.e. bijections with
@@ -83,6 +91,10 @@ infix 3 _⤖_
 
 _⤖_ : ∀ {f t} → Set f → Set t → Set _
 From ⤖ To = Bijection (P.setoid From) (P.setoid To)
+{-# WARNING_ON_USAGE _⤖_
+"Warning: _⤖_ was deprecated in v2.0.
+Please use Function.(Bundles.)mk⤖ instead."
+#-}
 
 bijection : ∀ {f t} {From : Set f} {To : Set t} →
             (to : From → To) (from : To → From) →
@@ -99,6 +111,11 @@ bijection to from inj invʳ = record
       }
     }
   }
+{-# WARNING_ON_USAGE bijection
+"Warning: bijection was deprecated in v2.0.
+Please use either Function.Properties.Bijection.trans or
+Function.Construct.Composition.bijection instead."
+#-}
 
 ------------------------------------------------------------------------
 -- Identity and composition. (Note that these proofs are superfluous,
@@ -112,6 +129,11 @@ id {S = S} = record
     ; surjective = Surjection.surjective (Surj.id {S = S})
     }
   }
+{-# WARNING_ON_USAGE id
+"Warning: id was deprecated in v2.0.
+Please use either Function.Properties.Bijection.refl or
+Function.Construct.Identity.bijection instead."
+#-}
 
 infixr 9 _∘_
 
@@ -125,3 +147,8 @@ f ∘ g = record
     ; surjective = Surjection.surjective (Surj._∘_ (surjection f) (surjection g))
     }
   } where open Bijection
+{-# WARNING_ON_USAGE _∘_
+"Warning: _∘_ was deprecated in v2.0.
+Please use either Function.Properties.Bijection.trans or
+Function.Construct.Composition.bijection instead."
+#-}

src/Function/Construct/Constant.agda

@@ -0,0 +1,64 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The constant function
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Function.Construct.Constant where
+
+open import Function.Base using (const)
+open import Function.Bundles
+import Function.Definitions as Definitions
+import Function.Structures as Structures
+open import Level using (Level)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures as B hiding (IsEquivalence)
+
+private
+  variable
+    a b ℓ₁ ℓ₂ : Level
+    A B : Set a
+
+------------------------------------------------------------------------
+-- Properties
+
+module _ (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂) where
+
+  open Definitions
+
+  congruent : ∀ {b} → b ≈₂ b → Congruent _≈₁_ _≈₂_ (const b)
+  congruent refl _ = refl
+
+------------------------------------------------------------------------
+-- Structures
+
+module _
+  {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂}
+  (isEq₁ : B.IsEquivalence ≈₁)
+  (isEq₂ : B.IsEquivalence ≈₂) where
+
+  open Structures ≈₁ ≈₂
+  open B.IsEquivalence
+
+  isCongruent : ∀ b → IsCongruent (const b)
+  isCongruent b = record
+    { cong           = congruent ≈₁ ≈₂ (refl isEq₂)
+    ; isEquivalence₁ = isEq₁
+    ; isEquivalence₂ = isEq₂
+    }
+
+------------------------------------------------------------------------
+-- Setoid bundles
+
+module _ (S : Setoid a ℓ₂) (T : Setoid b ℓ₂) where
+
+  open Setoid
+
+  function : Carrier T → Func S T
+  function b = record
+    { to   = const b
+    ; cong = congruent (_≈_ S) (_≈_ T) (refl T)
+    }

src/Function/Equality.agda

@@ -5,6 +5,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --warn=noUserWarning #-}
 
 module Function.Equality where
 
@@ -34,19 +35,31 @@ record Π {f₁ f₂ t₁ t₂}
   field
     _⟨$⟩_ : (x : Setoid.Carrier From) → IndexedSetoid.Carrier To x
     cong  : Setoid._≈_ From =[ _⟨$⟩_ ]⇒ IndexedSetoid._≈_ To
+{-# WARNING_ON_USAGE Π
+"Warning: Π was deprecated in v2.0.
+Please use Function.Dependent.Bundles.Func instead."
+#-}
 
 open Π public
 
 infixr 0 _⟶_
 
 _⟶_ : ∀ {f₁ f₂ t₁ t₂} → Setoid f₁ f₂ → Setoid t₁ t₂ → Set _
 From ⟶ To = Π From (Trivial.indexedSetoid To)
+{-# WARNING_ON_USAGE _⟶_
+"Warning: _⟶_ was deprecated in v2.0.
+Please use Function.(Bundles.)Func instead."
+#-}
 
 ------------------------------------------------------------------------
 -- Identity and composition.
 
 id : ∀ {a₁ a₂} {A : Setoid a₁ a₂} → A ⟶ A
 id = record { _⟨$⟩_ = Fun.id; cong = Fun.id }
+{-# WARNING_ON_USAGE id
+"Warning: id was deprecated in v2.0.
+Please use Function.Construct.Identity.function instead."
+#-}
 
 infixr 9 _∘_
 
@@ -58,6 +71,10 @@ f ∘ g = record
   { _⟨$⟩_ = Fun._∘_ (_⟨$⟩_ f) (_⟨$⟩_ g)
   ; cong  = Fun._∘_ (cong  f) (cong  g)
   }
+{-# WARNING_ON_USAGE _∘_
+"Warning: _∘_ was deprecated in v2.0.
+Please use Function.Construct.Composition.function instead."
+#-}
 
 -- Constant equality-preserving function.
 
@@ -68,6 +85,10 @@ const {B = B} b = record
   { _⟨$⟩_ = Fun.const b
   ; cong  = Fun.const (Setoid.refl B)
   }
+{-# WARNING_ON_USAGE const
+"Warning: const was deprecated in v2.0.
+Please use Function.Construct.Constant.function instead."
+#-}
 
 ------------------------------------------------------------------------
 -- Function setoids

src/Function/Equivalence.agda

@@ -31,6 +31,10 @@ record Equivalence {f₁ f₂ t₁ t₂}
   field
     to   : From ⟶ To
     from : To ⟶ From
+{-# WARNING_ON_USAGE Equivalence
+"Warning: Equivalence was deprecated in v2.0.
+Please use Function.(Bundles.)Equivalence instead."
+#-}
 
 ------------------------------------------------------------------------
 -- The set of all equivalences between two sets (i.e. equivalences
@@ -40,13 +44,21 @@ infix 3 _⇔_
 
 _⇔_ : ∀ {f t} → Set f → Set t → Set _
 From ⇔ To = Equivalence (P.setoid From) (P.setoid To)
+{-# WARNING_ON_USAGE _⇔_
+"Warning: _⇔_ was deprecated in v2.0.
+Please use Function.(Bundles.)_⇔_ instead."
+#-}
 
 equivalence : ∀ {f t} {From : Set f} {To : Set t} →
               (From → To) → (To → From) → From ⇔ To
 equivalence to from = record
   { to   = →-to-⟶ to
   ; from = →-to-⟶ from
   }
+{-# WARNING_ON_USAGE equivalence
+"Warning: equivalence was deprecated in v2.0.
+Please use Function.Properties.Equivalence.mkEquivalence instead."
+#-}
 
 ------------------------------------------------------------------------
 -- Equivalence is an equivalence relation
@@ -58,6 +70,11 @@ id {x = S} = record
   { to   = F.id
   ; from = F.id
   }
+{-# WARNING_ON_USAGE id
+"Warning: id was deprecated in v2.0.
+Please use Function.Properties.Equivalence.refl or
+Function.Construct.Identity.equivalence instead."
+#-}
 
 infixr 9 _∘_
 
@@ -69,6 +86,11 @@ f ∘ g = record
   { to   = to   f ⟪∘⟫ to   g
   ; from = from g ⟪∘⟫ from f
   } where open Equivalence
+{-# WARNING_ON_USAGE _∘_
+"Warning: _∘_ was deprecated in v2.0.
+Please use Function.Properties.Equivalence.trans or
+Function.Construct.Composition.equivalence instead."
+#-}
 
 -- Symmetry.
 
@@ -79,6 +101,11 @@ sym eq = record
   { from       = to
   ; to         = from
   } where open Equivalence eq
+{-# WARNING_ON_USAGE sym
+"Warning: sym was deprecated in v2.0.
+Please use Function.Properties.Equivalence.sym or
+Function.Construct.Symmetry.equivalence instead."
+#-}
 
 -- For fixed universe levels we can construct setoids.
 
@@ -92,6 +119,10 @@ setoid s₁ s₂ = record
     ; trans = flip _∘_
     }
   }
+{-# WARNING_ON_USAGE setoid
+"Warning: setoid was deprecated in v2.0.
+Please use Function.Properties.Equivalence.setoid instead."
+#-}
 
 ⇔-setoid : (ℓ : Level) → Setoid (suc ℓ) ℓ
 ⇔-setoid ℓ = record
@@ -103,6 +134,10 @@ setoid s₁ s₂ = record
     ; trans = flip _∘_
     }
   }
+{-# WARNING_ON_USAGE ⇔-setoid
+"Warning: ⇔-setoid was deprecated in v2.0.
+Please use Function.Properties.Equivalence.⇔-setoid instead."
+#-}
 
 ------------------------------------------------------------------------
 -- Transformations

src/Function/Injection.agda

@@ -7,11 +7,6 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 {-# OPTIONS --warn=noUserWarning #-}
 
--- Note: use of the standard function hierarchy is encouraged. The
--- module `Function` re-exports `Injective`, `IsInjection` and
--- `Injection`. The alternative definitions found in this file will
--- eventually be deprecated.
-
 module Function.Injection where
 
 {-# WARNING_ON_IMPORT
@@ -35,6 +30,10 @@ Injective {A = A} {B} f = ∀ {x y} → f ⟨$⟩ x ≈₂ f ⟨$⟩ y → x ≈
   where
   open Setoid A renaming (_≈_ to _≈₁_)
   open Setoid B renaming (_≈_ to _≈₂_)
+{-# WARNING_ON_USAGE Injective
+"Warning: Injective was deprecated in v2.0.
+Please use Function.(Definitions.)Injective instead."
+#-}
 
 ------------------------------------------------------------------------
 -- The set of all injections between two setoids
@@ -47,6 +46,10 @@ record Injection {f₁ f₂ t₁ t₂}
     injective : Injective to
 
   open Π to public
+{-# WARNING_ON_USAGE Injection
+"Warning: Injection was deprecated in v2.0.
+Please use Function.(Bundles.)Injection instead."
+#-}
 
 ------------------------------------------------------------------------
 -- The set of all injections from one set to another (i.e. injections
@@ -56,6 +59,10 @@ infix 3 _↣_
 
 _↣_ : ∀ {f t} → Set f → Set t → Set _
 From ↣ To = Injection (P.setoid From) (P.setoid To)
+{-# WARNING_ON_USAGE _↣_
+"Warning: _↣_ was deprecated in v2.0.
+Please use Function.(Bundles.)_↣_ instead."
+#-}
 
 injection : ∀ {f t} {From : Set f} {To : Set t} → (to : From → To) →
             (∀ {x y} → to x ≡ to y → x ≡ y) → From ↣ To
@@ -66,6 +73,10 @@ injection to injective = record
     }
   ; injective = injective
   }
+{-# WARNING_ON_USAGE injection
+"Warning: injection was deprecated in v2.0.
+Please use Function.(Bundles.)mk↣ instead."
+#-}
 
 ------------------------------------------------------------------------
 -- Identity and composition.
@@ -77,6 +88,11 @@ id = record
   { to        = F.id
   ; injective = Fun.id
   }
+{-# WARNING_ON_USAGE id
+"Warning: id was deprecated in v2.0.
+Please use Function.Properties.Injection.refl or
+Function.Construct.Identity.injection instead."
+#-}
 
 _∘_ : ∀ {f₁ f₂ m₁ m₂ t₁ t₂}
         {F : Setoid f₁ f₂} {M : Setoid m₁ m₂} {T : Setoid t₁ t₂} →
@@ -85,3 +101,8 @@ f ∘ g = record
   { to        =          to        f  ⟪∘⟫ to        g
   ; injective = (λ {_} → injective g) ⟨∘⟩ injective f
   } where open Injection
+{-# WARNING_ON_USAGE _∘_
+"Warning: _∘_ was deprecated in v2.0.
+Please use Function.Properties.Injection.trans or
+Function.Construct.Composition.injection instead."
+#-}