From 44384cabdcb0ce0e27e77746206b6a6a29c3caf1 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Mon, 12 Jun 2023 12:50:58 -0400 Subject: [PATCH 1/6] =?UTF-8?q?Migrate=20`=5F=E2=86=94=CC=87=5F`=20to=20th?= =?UTF-8?q?e=20new=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. From f913f55ec9d39bb775067141a99af8e9f55d4f75 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Wed, 14 Jun 2023 12:22:59 -0400 Subject: [PATCH 2/6] Add more indexed version of arrows --- CHANGELOG.md | 6 ++++ src/Algebra/Definitions.agda | 2 +- src/Function/Bundles.agda | 5 +-- src/Function/Indexed/Bundles.agda | 52 +++++++++++++++++++++++++++++++ 4 files changed, 60 insertions(+), 5 deletions(-) create mode 100644 src/Function/Indexed/Bundles.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index d5ba31beaf..3305d3ddf8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1595,6 +1595,12 @@ New modules ``` Algebra.Properties.KleeneAlgebra ``` + +* Relations on indexed sets + ``` + Function.Indexed.Bundles + ``` + Other minor changes ------------------- diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index c0820fafb7..e64fc4f30b 100644 --- a/src/Algebra/Definitions.agda +++ b/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 _ diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index e16cc550db..f314ba7bcc 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -313,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) @@ -341,9 +341,6 @@ 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. diff --git a/src/Function/Indexed/Bundles.agda b/src/Function/Indexed/Bundles.agda new file mode 100644 index 0000000000..8b9acc3efd --- /dev/null +++ b/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 From 4cf5ba0ee0326a593a3c21778cb4f5c624a44337 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Wed, 14 Jun 2023 12:23:58 -0400 Subject: [PATCH 3/6] Redundant import --- src/Function/Bundles.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index f314ba7bcc..6284182845 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -29,7 +29,6 @@ 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 From ed20bdce8246f9499f1dee3e84bda4a25f4c2708 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Wed, 14 Jun 2023 21:35:12 -0400 Subject: [PATCH 4/6] Try commenting the failing arrow --- src/Function/Indexed/Bundles.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Function/Indexed/Bundles.agda b/src/Function/Indexed/Bundles.agda index 8b9acc3efd..56e56849ec 100644 --- a/src/Function/Indexed/Bundles.agda +++ b/src/Function/Indexed/Bundles.agda @@ -23,7 +23,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where -- Bundles specialised for lifting relations to indexed sets ------------------------------------------------------------------------ -infix 3 _⟶ᵢ_ _↣ᵢ_ _↠ᵢ_ _⤖ᵢ_ _⇔ᵢ_ _↩ᵢ_ _↪ᵢ_ _↩↪ᵢ_ _↔ᵢ_ +infix 3 _⟶ᵢ_ _↣ᵢ_ _↠ᵢ_ _⤖ᵢ_ _⇔ᵢ_ _↩ᵢ_ _↪ᵢ_ _↔ᵢ_ _⟶ᵢ_ : ∀ {i} {I : Set i} → Pred I a → Pred I b → Set _ A ⟶ᵢ B = ∀ {i} → A i ⟶ B i @@ -45,8 +45,8 @@ 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 From 1051f4a87bbe6479542cbd6f3b3691d30b56b691 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Thu, 15 Jun 2023 15:14:09 -0400 Subject: [PATCH 5/6] Fix checks --- src/Function/Indexed/Bundles.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Function/Indexed/Bundles.agda b/src/Function/Indexed/Bundles.agda index 56e56849ec..306e9e5dad 100644 --- a/src/Function/Indexed/Bundles.agda +++ b/src/Function/Indexed/Bundles.agda @@ -23,7 +23,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where -- Bundles specialised for lifting relations to indexed sets ------------------------------------------------------------------------ -infix 3 _⟶ᵢ_ _↣ᵢ_ _↠ᵢ_ _⤖ᵢ_ _⇔ᵢ_ _↩ᵢ_ _↪ᵢ_ _↔ᵢ_ +infix 3 _⟶ᵢ_ _↣ᵢ_ _↠ᵢ_ _⤖ᵢ_ _⇔ᵢ_ _↩ᵢ_ _↪ᵢ_ _↩↪ᵢ_ _↔ᵢ_ _⟶ᵢ_ : ∀ {i} {I : Set i} → Pred I a → Pred I b → Set _ A ⟶ᵢ B = ∀ {i} → A i ⟶ B i @@ -45,8 +45,8 @@ 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 From 22992b9146230bc4d742a3ce178c784f04807032 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Fri, 16 Jun 2023 21:08:47 -0400 Subject: [PATCH 6/6] Module not required --- src/Function/Indexed/Bundles.agda | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Function/Indexed/Bundles.agda b/src/Function/Indexed/Bundles.agda index 306e9e5dad..033cabd426 100644 --- a/src/Function/Indexed/Bundles.agda +++ b/src/Function/Indexed/Bundles.agda @@ -17,8 +17,6 @@ private variable a b ℓ₁ ℓ₂ : Level -module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where - ------------------------------------------------------------------------ -- Bundles specialised for lifting relations to indexed sets ------------------------------------------------------------------------