From 70f9bdbee2894a6ab1fc2e7d906dc8948143ee55 Mon Sep 17 00:00:00 2001
From: = <matthewdaggitt@gmail.com>
Date: Sun, 3 May 2020 10:49:53 +0800
Subject: [PATCH] Added pseudo-deprecation warnings to old function
 infrastructure

---
 src/Function/Bijection.agda   | 5 +++++
 src/Function/Equality.agda    | 5 +++++
 src/Function/Equivalence.agda | 7 ++++++-
 src/Function/Injection.agda   | 5 +++++
 src/Function/Inverse.agda     | 5 +++++
 src/Function/LeftInverse.agda | 5 +++++
 src/Function/Surjection.agda  | 5 +++++
 7 files changed, 36 insertions(+), 1 deletion(-)

diff --git a/src/Function/Bijection.agda b/src/Function/Bijection.agda
index 9971cee7f3..80f1d5cc6d 100644
--- a/src/Function/Bijection.agda
+++ b/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
diff --git a/src/Function/Equality.agda b/src/Function/Equality.agda
index 26597f545a..f1e085f055 100644
--- a/src/Function/Equality.agda
+++ b/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
diff --git a/src/Function/Equivalence.agda b/src/Function/Equivalence.agda
index b6c0d113e8..6f371b8b98 100644
--- a/src/Function/Equivalence.agda
+++ b/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
diff --git a/src/Function/Injection.agda b/src/Function/Injection.agda
index fbb4c9e8cb..fe094a21a7 100644
--- a/src/Function/Injection.agda
+++ b/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 _⟨∘⟩_)
diff --git a/src/Function/Inverse.agda b/src/Function/Inverse.agda
index 472124eb97..c2e478a7f6 100644
--- a/src/Function/Inverse.agda
+++ b/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
diff --git a/src/Function/LeftInverse.agda b/src/Function/LeftInverse.agda
index 570b2d81b6..1942130a1e 100644
--- a/src/Function/LeftInverse.agda
+++ b/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
diff --git a/src/Function/Surjection.agda b/src/Function/Surjection.agda
index df3ac23248..5fe98844b9 100644
--- a/src/Function/Surjection.agda
+++ b/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