Migrate _↔̇_ to the new Function hierarchy + more arrows for indexed sets

CHANGELOG.md

@@ -1595,6 +1595,12 @@ New modules
   ```
   Algebra.Properties.KleeneAlgebra
   ```
+
+* Relations on indexed sets
+  ```
+  Function.Indexed.Bundles
+  ```
+
 Other minor changes
 -------------------
 

src/Algebra/Definitions.agda

@@ -109,7 +109,7 @@ _DistributesOver_ : Op₂ A → Op₂ A → Set _
 * DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +)
 
 _MiddleFourExchange_ : Op₂ A → Op₂ A → Set _
-_*_ MiddleFourExchange _+_ = 
+_*_ MiddleFourExchange _+_ =
   ∀ w x y z → ((w + x) * (y + z)) ≈ ((w + y) * (x + z))
 
 _IdempotentOn_ : Op₂ A → A → Set _

src/Function/Indexed/Bundles.agda

@@ -0,0 +1,52 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Operations on Relations for Indexed sets
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Function.Indexed.Bundles where
+
+open import Relation.Unary using (Pred)
+open import Function.Bundles using (_⟶_; _↣_; _↠_; _⤖_; _⇔_; _↩_; _↪_; _↩↪_; _↔_)
+open import Relation.Binary hiding (_⇔_)
+open import Level using (Level)
+
+private
+  variable
+    a b ℓ₁ ℓ₂ : Level
+
+module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
+
+------------------------------------------------------------------------
+-- Bundles specialised for lifting relations to indexed sets
+------------------------------------------------------------------------
+
+infix 3 _⟶ᵢ_ _↣ᵢ_ _↠ᵢ_ _⤖ᵢ_ _⇔ᵢ_ _↩ᵢ_ _↪ᵢ_ _↔ᵢ_
+_⟶ᵢ_ : ∀ {i} {I : Set i} → Pred I a → Pred I b → Set _
+A ⟶ᵢ B = ∀ {i} → A i ⟶ B i
+
+_↣ᵢ_ : ∀ {i} {I : Set i} → Pred I a → Pred I b → Set _
+A ↣ᵢ B = ∀ {i} → A i ↣ B i
+
+_↠ᵢ_ : ∀ {i} {I : Set i} → Pred I a → Pred I b → Set _
+A ↠ᵢ B = ∀ {i} → A i ↠ B i
+
+_⤖ᵢ_ : ∀ {i} {I : Set i} → Pred I a → Pred I b → Set _
+A ⤖ᵢ B = ∀ {i} → A i ⤖ B i
+
+_⇔ᵢ_ : ∀ {i} {I : Set i} → Pred I a → Pred I b → Set _
+A ⇔ᵢ B = ∀ {i} → A i ⇔ B i
+
+_↩ᵢ_ : ∀ {i} {I : Set i} → Pred I a → Pred I b → Set _
+A ↩ᵢ B = ∀ {i} → A i ↩ B i
+
+_↪ᵢ_ : ∀ {i} {I : Set i} → Pred I a → Pred I b → Set _
+A ↪ᵢ B = ∀ {i} → A i ↪ B i
+
+-- _↩↪ᵢ_ : ∀ {i} {I : Set i} ↩↪ Pred I a → Pred I b → Set _
+-- A ↩↪ᵢ B = ∀ {i} → A i ↩↪ B i
+
+_↔ᵢ_ : ∀ {i} {I : Set i} → Pred I a → Pred I b → Set _
+A ↔ᵢ B = ∀ {i} → A i ↔ B i