diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2dcdb3d924..e7d43ec18f 100644
--- a/CHANGELOG.md
+++ b/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
diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda
index 9866971920..f290c7341b 100644
--- a/src/Data/Product/Function/Dependent/Setoid.agda
+++ b/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
diff --git a/src/Function/Bijection.agda b/src/Function/Bijection.agda
index bb7f2d2cce..ac32159e7a 100644
--- a/src/Function/Bijection.agda
+++ b/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."
+#-}
diff --git a/src/Function/Construct/Constant.agda b/src/Function/Construct/Constant.agda
new file mode 100644
index 0000000000..2f43929a87
--- /dev/null
+++ b/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)
+    }
diff --git a/src/Function/Equality.agda b/src/Function/Equality.agda
index 4ce068b45c..7451aaf3f7 100644
--- a/src/Function/Equality.agda
+++ b/src/Function/Equality.agda
@@ -5,6 +5,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --warn=noUserWarning #-}
 
 module Function.Equality where
 
@@ -34,6 +35,10 @@ 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
 
@@ -41,12 +46,20 @@ 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
diff --git a/src/Function/Equivalence.agda b/src/Function/Equivalence.agda
index b25f2a062f..1e3652da7f 100644
--- a/src/Function/Equivalence.agda
+++ b/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,6 +44,10 @@ 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
@@ -47,6 +55,10 @@ 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
diff --git a/src/Function/Injection.agda b/src/Function/Injection.agda
index 910c91aa35..462b8b3428 100644
--- a/src/Function/Injection.agda
+++ b/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."
+#-}
diff --git a/src/Function/Inverse.agda b/src/Function/Inverse.agda
index e2cb395ea5..e9d796eddf 100644
--- a/src/Function/Inverse.agda
+++ b/src/Function/Inverse.agda
@@ -35,6 +35,10 @@ record _InverseOf_ {f₁ f₂ t₁ t₂}
   field
     left-inverse-of  : from LeftInverseOf  to
     right-inverse-of : from RightInverseOf to
+{-# WARNING_ON_USAGE _InverseOf_
+"Warning: _InverseOf_ was deprecated in v2.0.
+Please use Function.(Structures.)IsInverse instead."
+#-}
 
 ------------------------------------------------------------------------
 -- The set of all inverses between two setoids
@@ -74,6 +78,10 @@ record Inverse {f₁ f₂ t₁ t₂}
   open Bijection bijection public
     using (equivalence; surjective; surjection; right-inverse;
            to-from; from-to)
+{-# WARNING_ON_USAGE Inverse
+"Warning: Inverse was deprecated in v2.0.
+Please use Function.(Bundles.)Inverse instead."
+#-}
 
 ------------------------------------------------------------------------
 -- The set of all inverses between two sets (i.e. inverses with
@@ -83,9 +91,17 @@ infix 3 _↔_ _↔̇_
 
 _↔_ : ∀ {f t} → Set f → Set t → Set _
 From ↔ To = Inverse (P.setoid From) (P.setoid To)
+{-# WARNING_ON_USAGE _↔_
+"Warning: _↔_ was deprecated in v2.0.
+Please use Function.(Bundles.)_↔_ instead."
+#-}
 
 _↔̇_ : ∀ {i f t} {I : Set i} → Pred I f → Pred I t → Set _
 From ↔̇ To = ∀ {i} → From i ↔ To i
+{-# WARNING_ON_USAGE _↔̇_
+"Warning: _↔̇_ was deprecated in v2.0.
+Please use Function.Indexed.(Bundles.)_↔ᵢ_ instead."
+#-}
 
 inverse : ∀ {f t} {From : Set f} {To : Set t} →
           (to : From → To) (from : To → From) →
@@ -100,6 +116,10 @@ inverse to from from∘to to∘from = record
     ; right-inverse-of = to∘from
     }
   }
+{-# WARNING_ON_USAGE inverse
+"Warning: inverse was deprecated in v2.0.
+Please use Function.(Bundles.)mk↔ instead."
+#-}
 
 ------------------------------------------------------------------------
 -- If two setoids are in bijective correspondence, then there is an
@@ -131,6 +151,11 @@ id {x = S} = record
     ; right-inverse-of = LeftInverse.left-inverse-of id′
     }
   } where id′ = Left.id {S = S}
+{-# WARNING_ON_USAGE id
+"Warning: id was deprecated in v2.0.
+Please use either Function.Properties.Inverse.refl or
+Function.Construct.Identity.inverse instead."
+#-}
 
 -- Transitivity
 
@@ -148,6 +173,11 @@ f ∘ g = record
     ; right-inverse-of = LeftInverse.left-inverse-of (Left._∘_ (right-inverse g) (right-inverse f))
     }
   } where open Inverse
+{-# WARNING_ON_USAGE _∘_
+"Warning: _∘_ was deprecated in v2.0.
+Please use either Function.Properties.Inverse.trans or
+Function.Construct.Composition.inverse instead."
+#-}
 
 -- Symmetry.
 
@@ -161,6 +191,11 @@ sym inv = record
     ; right-inverse-of = left-inverse-of
     }
   } where open Inverse inv
+{-# WARNING_ON_USAGE sym
+"Warning: sym was deprecated in v2.0.
+Please use either Function.Properties.Inverse.sym or
+Function.Construct.Symmetry.inverse instead."
+#-}
 
 ------------------------------------------------------------------------
 -- Transformations
diff --git a/src/Function/LeftInverse.agda b/src/Function/LeftInverse.agda
index 7ff0fda218..3824ca95d3 100644
--- a/src/Function/LeftInverse.agda
+++ b/src/Function/LeftInverse.agda
@@ -31,11 +31,19 @@ _LeftInverseOf_ :
   To ⟶ From → From ⟶ To → Set _
 _LeftInverseOf_ {From = From} f g = ∀ x → f ⟨$⟩ (g ⟨$⟩ x) ≈ x
   where open Setoid From
+{-# WARNING_ON_USAGE _LeftInverseOf_
+"Warning: _LeftInverseOf_ was deprecated in v2.0.
+Please use Function.(Structures.)IsRightInverse instead."
+#-}
 
 _RightInverseOf_ :
   ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
   To ⟶ From → From ⟶ To → Set _
 f RightInverseOf g = g LeftInverseOf f
+{-# WARNING_ON_USAGE _RightInverseOf_
+"Warning: _RightInverseOf_ was deprecated in v2.0.
+Please use Function.(Structures.)IsLeftInverse instead."
+#-}
 
 ------------------------------------------------------------------------
 -- The set of all left inverses between two setoids.
@@ -74,12 +82,20 @@ record LeftInverse {f₁ f₂ t₁ t₂}
     from ⟨$⟩ y           ≈⟨ Eq.cong from (T.sym to-x≈y) ⟩
     from ⟨$⟩ (to ⟨$⟩ x)  ≈⟨ left-inverse-of x ⟩
     x                    ∎
+{-# WARNING_ON_USAGE LeftInverse
+"Warning: LeftInverse was deprecated in v2.0.
+Please use Function.(Bundles.)RightInverse instead."
+#-}
 
 -- The set of all right inverses between two setoids.
 
 RightInverse : ∀ {f₁ f₂ t₁ t₂}
                (From : Setoid f₁ f₂) (To : Setoid t₁ t₂) → Set _
 RightInverse From To = LeftInverse To From
+{-# WARNING_ON_USAGE RightInverse
+"Warning: RightInverse was deprecated in v2.0.
+Please use Function.(Bundles.)LeftInverse instead."
+#-}
 
 ------------------------------------------------------------------------
 -- The set of all left inverses from one set to another (i.e. left
@@ -91,6 +107,10 @@ infix 3 _↞_
 
 _↞_ : ∀ {f t} → Set f → Set t → Set _
 From ↞ To = LeftInverse (P.setoid From) (P.setoid To)
+{-# WARNING_ON_USAGE _↞_
+"Warning: _↞_ was deprecated in v2.0.
+Please use Function.(Bundles.)_↪_ instead."
+#-}
 
 leftInverse : ∀ {f t} {From : Set f} {To : Set t} →
               (to : From → To) (from : To → From) →
@@ -101,6 +121,10 @@ leftInverse to from invˡ = record
   ; from            = Eq.→-to-⟶ from
   ; left-inverse-of = invˡ
   }
+{-# WARNING_ON_USAGE leftInverse
+"Warning: leftInverse was deprecated in v2.0.
+Please use Function.(Bundles.)mk↪ instead."
+#-}
 
 ------------------------------------------------------------------------
 -- Identity and composition.
@@ -111,6 +135,11 @@ id {S = S} = record
   ; from            = Eq.id
   ; left-inverse-of = λ _ → Setoid.refl S
   }
+{-# WARNING_ON_USAGE id
+"Warning: id was deprecated in v2.0.
+Please use either Function.Properties.RightInverse.refl or
+Function.Construct.Identity.rightInverse instead."
+#-}
 
 infixr 9 _∘_
 
@@ -128,3 +157,8 @@ _∘_ {F = F} f g = record
   where
   open LeftInverse
   open EqReasoning F
+{-# WARNING_ON_USAGE _∘_
+"Warning: _∘_ was deprecated in v2.0.
+Please use either Function.Properties.RightInverse.trans or
+Function.Construct.Composition.rightInverse instead."
+#-}
diff --git a/src/Function/Properties/Equivalence.agda b/src/Function/Properties/Equivalence.agda
index 308a29525d..ad1264ec7c 100644
--- a/src/Function/Properties/Equivalence.agda
+++ b/src/Function/Properties/Equivalence.agda
@@ -11,6 +11,7 @@ module Function.Properties.Equivalence where
 
 open import Function.Bundles
 open import Level
+open import Relation.Binary.Definitions
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Structures using (IsEquivalence)
 import Relation.Binary.PropositionalEquality.Properties as Eq
@@ -21,7 +22,7 @@ import Function.Construct.Composition as Composition
 
 private
   variable
-    a ℓ : Level
+    a b c ℓ ℓ₁ ℓ₂ ℓ₃ : Level
     A B : Set a
     S T : Setoid a ℓ
 
@@ -36,13 +37,37 @@ mkEquivalence f g = record
   ; from-cong = cong g
   } where open Func
 
+⟶×⟵⇒⇔ : A ⟶ B → B ⟶ A → A ⇔ B
+⟶×⟵⇒⇔ = mkEquivalence
+
+------------------------------------------------------------------------
+-- Destructors
+
+⇔⇒⟶ : A ⇔ B → A ⟶ B
+⇔⇒⟶ = Equivalence.toFunction
+
+⇔⇒⟵ : A ⇔ B → B ⟶ A
+⇔⇒⟵ = Equivalence.fromFunction
+
 ------------------------------------------------------------------------
 -- Setoid bundles
 
+refl : Reflexive (Equivalence {a} {ℓ})
+refl {x = x} = Identity.equivalence x
+
+sym : Sym (Equivalence {a} {ℓ₁} {b} {ℓ₂})
+          (Equivalence {b} {ℓ₂} {a} {ℓ₁})
+sym = Symmetry.equivalence
+
+trans : Trans (Equivalence {a} {ℓ₁} {b} {ℓ₂})
+              (Equivalence {b} {ℓ₂} {c} {ℓ₃})
+              (Equivalence {a} {ℓ₁} {c} {ℓ₃})
+trans = Composition.equivalence
+
 isEquivalence : IsEquivalence (Equivalence {a} {ℓ})
 isEquivalence = record
-  { refl = λ {x} → Identity.equivalence x
-  ; sym = Symmetry.equivalence
+  { refl = refl
+  ; sym = sym
   ; trans = Composition.equivalence
   }
 
@@ -69,12 +94,3 @@ setoid s₁ s₂ = record
   ; _≈_           = _⇔_
   ; isEquivalence = ⇔-isEquivalence
   }
-
-⟶×⟵⇒⇔ : A ⟶ B → B ⟶ A → A ⇔ B
-⟶×⟵⇒⇔ = mkEquivalence
-
-⇔⇒⟶ : A ⇔ B → A ⟶ B
-⇔⇒⟶ = Equivalence.toFunction
-
-⇔⇒⟵ : A ⇔ B → B ⟶ A
-⇔⇒⟵ = Equivalence.fromFunction
diff --git a/src/Function/Properties/Injection.agda b/src/Function/Properties/Injection.agda
index bca8ac4dc5..0e773cf9b8 100644
--- a/src/Function/Properties/Injection.agda
+++ b/src/Function/Properties/Injection.agda
@@ -15,13 +15,14 @@ import Function.Construct.Identity as Identity
 import Function.Construct.Composition as Compose
 open import Level using (Level)
 open import Data.Product.Base using (proj₁; proj₂)
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Definitions
+open import Relation.Binary.PropositionalEquality using ()
 open import Relation.Binary using (Setoid)
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 
 private
   variable
-    a b ℓ : Level
+    a b c ℓ ℓ₁ ℓ₂ ℓ₃ : Level
     A B : Set a
     T S U : Setoid a ℓ
 
@@ -43,10 +44,21 @@ mkInjection f injective = record
 ↣⇒⟶ = Injection.function
 
 ------------------------------------------------------------------------
--- Properties
+-- Setoid properties
+
+refl : Reflexive (Injection {a} {ℓ})
+refl {x = x} = Identity.injection x
+
+trans : Trans (Injection {a} {ℓ₁} {b} {ℓ₂})
+              (Injection {b} {ℓ₂} {c} {ℓ₃})
+              (Injection {a} {ℓ₁} {c} {ℓ₃})
+trans = Compose.injection
+
+------------------------------------------------------------------------
+-- Propositonal properties
 
 ↣-refl : Injection S S
-↣-refl = Identity.injection _
+↣-refl = refl
 
 ↣-trans : Injection S T → Injection T U → Injection S U
-↣-trans = Compose.injection
+↣-trans = trans
diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda
index d16670639c..5c2b235506 100644
--- a/src/Function/Properties/Surjection.agda
+++ b/src/Function/Properties/Surjection.agda
@@ -11,15 +11,18 @@ module Function.Properties.Surjection where
 open import Function.Base
 open import Function.Definitions
 open import Function.Bundles
+import Function.Construct.Identity as Identity
+import Function.Construct.Composition as Compose
 open import Level using (Level)
 open import Data.Product.Base using (proj₁; proj₂)
-open import Relation.Binary.PropositionalEquality
-open import Relation.Binary using (Setoid)
+import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.Definitions
+open import Relation.Binary.Bundles using (Setoid)
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 
 private
   variable
-    a b ℓ : Level
+    a b c ℓ ℓ₁ ℓ₂ ℓ₃ : Level
     A B : Set a
     T S : Setoid a ℓ
 
@@ -41,13 +44,24 @@ mkSurjection f surjective = record
 ↠⇒⟶ = Surjection.function
 
 ↠⇒↪ : A ↠ B → B ↪ A
-↠⇒↪ s = mk↪ {from = to} λ { refl → proj₂ (strictlySurjective _)}
+↠⇒↪ s = mk↪ {from = to} λ { P.refl → proj₂ (strictlySurjective _)}
   where open Surjection s
 
 ↠⇒⇔ : A ↠ B → A ⇔ B
 ↠⇒⇔ s = mk⇔ to (proj₁ ∘ surjective)
   where open Surjection s
 
+------------------------------------------------------------------------
+-- Setoid properties
+
+refl : Reflexive (Surjection {a} {ℓ})
+refl {x = x} = Identity.surjection x
+
+trans : Trans (Surjection {a} {ℓ₁} {b} {ℓ₂})
+              (Surjection {b} {ℓ₂} {c} {ℓ₃})
+              (Surjection {a} {ℓ₁} {c} {ℓ₃})
+trans = Compose.surjection
+
 ------------------------------------------------------------------------
 -- Other
 
diff --git a/src/Function/Surjection.agda b/src/Function/Surjection.agda
index bd96c50efb..2fdfefa9af 100644
--- a/src/Function/Surjection.agda
+++ b/src/Function/Surjection.agda
@@ -33,6 +33,10 @@ record Surjective {f₁ f₂ t₁ t₂}
   field
     from             : To ⟶ From
     right-inverse-of : from RightInverseOf to
+{-# WARNING_ON_USAGE Surjective
+"Warning: Surjective was deprecated in v2.0.
+Please use Function.(Definitions.)Surjective instead."
+#-}
 
 ------------------------------------------------------------------------
 -- The set of all surjections from one setoid to another.
@@ -67,6 +71,10 @@ record Surjection {f₁ f₂ t₁ t₂}
     { to   = to
     ; from = from
     }
+{-# WARNING_ON_USAGE Surjection
+"Warning: Surjection was deprecated in v2.0.
+Please use Function.(Bundles.)Surjection instead."
+#-}
 
 -- Right inverses can be turned into surjections.
 
@@ -80,6 +88,10 @@ fromRightInverse r = record
     ; right-inverse-of = left-inverse-of
     }
   } where open LeftInverse r
+{-# WARNING_ON_USAGE fromRightInverse
+"Warning: fromRightInverse was deprecated in v2.0.
+Please use Function.(Properties.)RightInverse.RightInverse⇒Surjection instead."
+#-}
 
 ------------------------------------------------------------------------
 -- The set of all surjections from one set to another (i.e. sujections
@@ -89,6 +101,10 @@ infix 3 _↠_
 
 _↠_ : ∀ {f t} → Set f → Set t → Set _
 From ↠ To = Surjection (P.setoid From) (P.setoid To)
+{-# WARNING_ON_USAGE _↠_
+"Warning: _↠_ was deprecated in v2.0.
+Please use Function.(Bundles.)_↠_ instead."
+#-}
 
 surjection : ∀ {f t} {From : Set f} {To : Set t} →
              (to : From → To) (from : To → From) →
@@ -101,6 +117,10 @@ surjection to from surjective = record
     ; right-inverse-of = surjective
     }
   }
+{-# WARNING_ON_USAGE surjection
+"Warning: surjection was deprecated in v2.0.
+Please use Function.(Bundles.)mk↠ instead."
+#-}
 
 ------------------------------------------------------------------------
 -- Identity and composition.
@@ -113,6 +133,11 @@ id {S = S} = record
     ; right-inverse-of = LeftInverse.left-inverse-of id′
     }
   } where id′ = Left.id {S = S}
+{-# WARNING_ON_USAGE id
+"Warning: id was deprecated in v2.0.
+Please use Function.Properties.Surjection.refl or
+Function.Construct.Identity.surjection instead."
+#-}
 
 infixr 9 _∘_
 
@@ -129,3 +154,8 @@ f ∘ g = record
   where
   open Surjection
   g∘f = Left._∘_ (right-inverse g) (right-inverse f)
+{-# WARNING_ON_USAGE _∘_
+"Warning: _∘_ was deprecated in v2.0.
+Please use Function.Properties.Surjection.trans or
+Function.Construct.Composition.surjection instead."
+#-}