Added pseudo-deprecation warnings to old function infrastructure

src/Function/Bijection.agda

@@ -6,6 +6,11 @@
 
 {-# OPTIONS --without-K --safe #-}
 
+-- Note: use of the standard function hierarchy is encouraged. The
+-- module `Function` re-exports `Bijective`, `IsBijection` and
+-- `Bijection`. The alternative definitions found in this file will
+-- eventually be deprecated.
+
 module Function.Bijection where
 
 open import Data.Product

src/Function/Equality.agda

@@ -6,6 +6,11 @@
 
 {-# OPTIONS --without-K --safe #-}
 
+-- Note: use of the standard function hierarchy is encouraged. The
+-- module `Function` re-exports `Congruent`, `IsBijection` and
+-- `Bijection`. The alternative definitions found in this file will
+-- eventually be deprecated.
+
 module Function.Equality where
 
 import Function.Base as Fun

src/Function/Equivalence.agda

@@ -8,7 +8,12 @@
 
 module Function.Equivalence where
 
-open import Function using (flip)
+-- Note: use of the standard function hierarchy is encouraged. The
+-- module `Function` re-exports `Congruent` and `IsCongruent`.
+-- The alternative definitions found in this file will eventually be
+-- deprecated.
+
+open import Function.Base using (flip)
 open import Function.Equality as F
   using (_⟶_; _⟨$⟩_) renaming (_∘_ to _⟪∘⟫_)
 open import Level

src/Function/Injection.agda

@@ -6,6 +6,11 @@
 
 {-# OPTIONS --without-K --safe #-}
 
+-- 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
 
 open import Function as Fun using () renaming (_∘_ to _⟨∘⟩_)

src/Function/Inverse.agda

@@ -6,6 +6,11 @@
 
 {-# OPTIONS --without-K --safe #-}
 
+-- Note: use of the standard function hierarchy is encouraged. The
+-- module `Function` re-exports `Inverseᵇ`, `IsInverse` and
+-- `Inverse`. The alternative definitions found in this file will
+-- eventually be deprecated.
+
 module Function.Inverse where
 
 open import Level

src/Function/LeftInverse.agda

@@ -6,6 +6,11 @@
 
 {-# OPTIONS --without-K --safe #-}
 
+-- Note: use of the standard function hierarchy is encouraged. The
+-- module `Function` re-exports `Inverseˡ`, `IsLeftInverse` and
+-- `LeftInverse`. The alternative definitions found in this file will
+-- eventually be deprecated.
+
 module Function.LeftInverse where
 
 open import Data.Product

src/Function/Surjection.agda

@@ -6,6 +6,11 @@
 
 {-# OPTIONS --without-K --safe #-}
 
+-- Note: use of the standard function hierarchy is encouraged. The
+-- module `Function` re-exports `Surjective`, `IsSurjection` and
+-- `Surjection`. The alternative definitions found in this file will
+-- eventually be deprecated.
+
 module Function.Surjection where
 
 open import Level