From 44384cabdcb0ce0e27e77746206b6a6a29c3caf1 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Mon, 12 Jun 2023 12:50:58 -0400
Subject: [PATCH] =?UTF-8?q?Migrate=20`=5F=E2=86=94=CC=87=5F`=20to=20the=20?=
 =?UTF-8?q?new=20Function=20hierarchy?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Function/Bundles.agda | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda
index 6284182845..e16cc550db 100644
--- a/src/Function/Bundles.agda
+++ b/src/Function/Bundles.agda
@@ -29,6 +29,7 @@ open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as ≡
 open Setoid using (isEquivalence)
+open import Relation.Unary using (Pred)
 
 private
   variable
@@ -312,7 +313,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
 -- Bundles specialised for propositional equality
 ------------------------------------------------------------------------
 
-infix 3 _⟶_ _↣_ _↠_ _⤖_ _⇔_ _↩_ _↪_ _↩↪_ _↔_
+infix 3 _⟶_ _↣_ _↠_ _⤖_ _⇔_ _↩_ _↪_ _↩↪_ _↔_ _↔̇_
 _⟶_ : Set a → Set b → Set _
 A ⟶ B = Func (≡.setoid A) (≡.setoid B)
 
@@ -340,6 +341,9 @@ A ↩↪ B = BiInverse (≡.setoid A) (≡.setoid B)
 _↔_ : Set a → Set b → Set _
 A ↔ B = Inverse (≡.setoid A) (≡.setoid B)
 
+_↔̇_ : ∀ {i} {I : Set i} → Pred I a → Pred I b → Set _
+A ↔̇ B = ∀ {i} → A i ↔ B i
+
 -- We now define some constructors for the above that
 -- automatically provide the required congruency proofs.