From cf181c4df47518575364b8cd9e9edd0bd69b64ad Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 28 Jan 2025 18:23:08 +0000 Subject: [PATCH 01/64] fixes #2568 --- .../Function/Dependent/Propositional.agda | 12 ++++++------ src/Data/Product/Function/Dependent/Setoid.agda | 4 ++-- src/Function/Bundles.agda | 13 ++++++++++--- src/Function/Construct/Composition.agda | 7 ++++--- src/Function/Construct/Symmetry.agda | 16 +++++++--------- src/Function/Properties/Bijection.agda | 4 ++-- src/Function/Properties/Surjection.agda | 14 +++++++------- src/Function/Structures.agda | 10 ++++++++-- 8 files changed, 46 insertions(+), 34 deletions(-) diff --git a/src/Data/Product/Function/Dependent/Propositional.agda b/src/Data/Product/Function/Dependent/Propositional.agda index 4c6f391e2f..8ec6cc8f9f 100644 --- a/src/Data/Product/Function/Dependent/Propositional.agda +++ b/src/Data/Product/Function/Dependent/Propositional.agda @@ -57,7 +57,7 @@ module _ where Σ I A ⇔ Σ J B Σ-⇔ {B = B} I↠J A⇔B = mk⇔ (map (to I↠J) (Equivalence.to A⇔B)) - (map (to⁻ I↠J) (Equivalence.from A⇔B ∘ ≡.subst B (≡.sym (proj₂ (surjective I↠J _) ≡.refl)))) + (map (section I↠J) (Equivalence.from A⇔B ∘ ≡.subst B (≡.sym (proj₂ (surjective I↠J _) ≡.refl)))) -- See also Data.Product.Relation.Binary.Pointwise.Dependent.WithK.↣. @@ -193,16 +193,16 @@ module _ where to′ : Σ I A → Σ J B to′ = map (to I↠J) (to A↠B) - backcast : ∀ {i} → B i → B (to I↠J (to⁻ I↠J i)) + backcast : ∀ {i} → B i → B (to I↠J (section I↠J i)) backcast = ≡.subst B (≡.sym (to∘to⁻ I↠J _)) to⁻′ : Σ J B → Σ I A - to⁻′ = map (to⁻ I↠J) (Surjection.to⁻ A↠B ∘ backcast) + to⁻′ = map (section I↠J) (Surjection.section A↠B ∘ backcast) strictlySurjective′ : StrictlySurjective _≡_ to′ strictlySurjective′ (x , y) = to⁻′ (x , y) , Σ-≡,≡→≡ ( to∘to⁻ I↠J x - , (≡.subst B (to∘to⁻ I↠J x) (to A↠B (to⁻ A↠B (backcast y))) ≡⟨ ≡.cong (≡.subst B _) (to∘to⁻ A↠B _) ⟩ + , (≡.subst B (to∘to⁻ I↠J x) (to A↠B (section A↠B (backcast y))) ≡⟨ ≡.cong (≡.subst B _) (to∘to⁻ A↠B _) ⟩ ≡.subst B (to∘to⁻ I↠J x) (backcast y) ≡⟨ ≡.subst-subst-sym (to∘to⁻ I↠J x) ⟩ y ∎) ) where open ≡.≡-Reasoning @@ -249,7 +249,7 @@ module _ where Σ I A ↔ Σ J B Σ-↔ {I = I} {J = J} {A = A} {B = B} I↔J A↔B = mk↔ₛ′ (Surjection.to surjection′) - (Surjection.to⁻ surjection′) + (Surjection.section surjection′) (Surjection.to∘to⁻ surjection′) left-inverse-of where @@ -260,7 +260,7 @@ module _ where surjection′ : Σ I A ↠ Σ J B surjection′ = Σ-↠ (↔⇒↠ (≃⇒↔ I≃J)) (↔⇒↠ A↔B) - left-inverse-of : ∀ p → Surjection.to⁻ surjection′ (Surjection.to surjection′ p) ≡ p + left-inverse-of : ∀ p → Surjection.section surjection′ (Surjection.to surjection′ p) ≡ p left-inverse-of (x , y) = to Σ-≡,≡↔≡ ( _≃_.left-inverse-of I≃J x , (≡.subst A (_≃_.left-inverse-of I≃J x) diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda index 0ad3785ed7..82442ac08f 100644 --- a/src/Data/Product/Function/Dependent/Setoid.agda +++ b/src/Data/Product/Function/Dependent/Setoid.agda @@ -117,7 +117,7 @@ module _ where B-to : ∀ {x} → Func (A atₛ x) (B atₛ (Surjection.to I↠J x)) B-to = toFunction A⇔B - B-from : ∀ {y} → Func (B atₛ y) (A atₛ (Surjection.to⁻ I↠J y)) + B-from : ∀ {y} → Func (B atₛ y) (A atₛ (Surjection.section I↠J y)) B-from = record { to = from A⇔B ∘ cast B (Surjection.to∘to⁻ I↠J _) ; cong = from-cong A⇔B ∘ cast-cong B (Surjection.to∘to⁻ I↠J _) @@ -169,7 +169,7 @@ module _ where func = function (Surjection.function I↠J) (Surjection.function A↠B) to⁻′ : Carrier (J ×ₛ B) → Carrier (I ×ₛ A) - to⁻′ (j , y) = to⁻ I↠J j , to⁻ A↠B (cast B (Surjection.to∘to⁻ I↠J _) y) + to⁻′ (j , y) = section I↠J j , section A↠B (cast B (Surjection.to∘to⁻ I↠J _) y) strictlySurj : StrictlySurjective (Func.Eq₂._≈_ func) (Func.to func) strictlySurj (j , y) = to⁻′ (j , y) , diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index 6532715a21..4fe0f97529 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -113,12 +113,17 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where open IsSurjection isSurjection public using ( strictlySurjective + ; section ) to⁻ : B → A to⁻ = proj₁ ∘ surjective + {-# WARNING_ON_USAGE to⁻ + "Warning: to⁻ was deprecated in v2.3. + Please use Function.Structures.IsSurjection.section instead. " + #-} - to∘to⁻ : ∀ x → to (to⁻ x) ≈₂ x + to∘to⁻ : ∀ x → to (section x) ≈₂ x to∘to⁻ = proj₂ ∘ strictlySurjective @@ -146,8 +151,10 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where ; surjective = surjective } - open Injection injection public using (isInjection) - open Surjection surjection public using (isSurjection; to⁻; strictlySurjective) + open Injection injection public + using (isInjection) + open Surjection surjection public + using (isSurjection; section; to∘to⁻; strictlySurjective) isBijection : IsBijection to isBijection = record diff --git a/src/Function/Construct/Composition.agda b/src/Function/Construct/Composition.agda index 10289cc8c9..799c0257c7 100644 --- a/src/Function/Construct/Composition.agda +++ b/src/Function/Construct/Composition.agda @@ -40,9 +40,10 @@ module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) (≈₃ : Rel C ℓ₃) surjective : Surjective ≈₁ ≈₂ f → Surjective ≈₂ ≈₃ g → Surjective ≈₁ ≈₃ (g ∘ f) - surjective f-sur g-sur x with g-sur x - ... | y , gproof with f-sur y - ... | z , fproof = z , gproof ∘ fproof + surjective f-sur g-sur x = + let y , gproof = g-sur x in + let z , fproof = f-sur y in + z , gproof ∘ fproof bijective : Bijective ≈₁ ≈₂ f → Bijective ≈₂ ≈₃ g → Bijective ≈₁ ≈₃ (g ∘ f) diff --git a/src/Function/Construct/Symmetry.agda b/src/Function/Construct/Symmetry.agda index e7e9f13db9..494197abbb 100644 --- a/src/Function/Construct/Symmetry.agda +++ b/src/Function/Construct/Symmetry.agda @@ -71,15 +71,14 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} private module IB = IsBijection isBij - f⁻¹ = proj₁ ∘ IB.surjective -- We can only flip a bijection if the witness produced by the -- surjection proof respects the equality on the codomain. - isBijection : Congruent ≈₂ ≈₁ f⁻¹ → IsBijection ≈₂ ≈₁ f⁻¹ - isBijection f⁻¹-cong = record + isBijection : Congruent ≈₂ ≈₁ IB.section → IsBijection ≈₂ ≈₁ IB.section + isBijection section-cong = record { isInjection = record { isCongruent = record - { cong = f⁻¹-cong + { cong = section-cong ; isEquivalence₁ = IB.Eq₂.isEquivalence ; isEquivalence₂ = IB.Eq₁.isEquivalence } @@ -93,7 +92,7 @@ module _ {≈₁ : Rel A ℓ₁} {f : A → B} (isBij : IsBijection ≈₁ _≡_ -- We can always flip a bijection if using the equality over the -- codomain is propositional equality. isBijection-≡ : IsBijection _≡_ ≈₁ _ - isBijection-≡ = isBijection isBij (IB.Eq₁.reflexive ∘ cong _) + isBijection-≡ = isBijection isBij (IB.Eq₁.reflexive ∘ cong IB.section) where module IB = IsBijection isBij module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} {f⁻¹ : B → A} where @@ -132,13 +131,12 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} (bij : Bijection R S) where private module IB = Bijection bij - from = proj₁ ∘ IB.surjective -- We can only flip a bijection if the witness produced by the -- surjection proof respects the equality on the codomain. - bijection : Congruent IB.Eq₂._≈_ IB.Eq₁._≈_ from → Bijection S R + bijection : Congruent IB.Eq₂._≈_ IB.Eq₁._≈_ IB.section → Bijection S R bijection cong = record - { to = from + { to = IB.section ; cong = cong ; bijective = bijective IB.bijective IB.Eq₁.refl IB.Eq₂.sym IB.Eq₂.trans IB.cong } @@ -191,7 +189,7 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} where -- Propositional bundles ⤖-sym : A ⤖ B → B ⤖ A -⤖-sym b = bijection b (cong _) +⤖-sym b = bijection b (cong section) where open Bijection b using (section) ⇔-sym : A ⇔ B → B ⇔ A ⇔-sym = equivalence diff --git a/src/Function/Properties/Bijection.agda b/src/Function/Properties/Bijection.agda index 21e295e807..4219006ec0 100644 --- a/src/Function/Properties/Bijection.agda +++ b/src/Function/Properties/Bijection.agda @@ -60,13 +60,13 @@ trans = Composition.bijection Bijection⇒Inverse : Bijection S T → Inverse S T Bijection⇒Inverse bij = record { to = to - ; from = to⁻ + ; from = section ; to-cong = cong ; from-cong = injective⇒to⁻-cong surjection injective ; inverse = (λ y≈to⁻[x] → Eq₂.trans (cong y≈to⁻[x]) (to∘to⁻ _)) , (λ y≈to[x] → injective (Eq₂.trans (to∘to⁻ _) y≈to[x])) } - where open Bijection bij; to∘to⁻ = proj₂ ∘ strictlySurjective + where open Bijection bij Bijection⇒Equivalence : Bijection T S → Equivalence T S Bijection⇒Equivalence = Inverse⇒Equivalence ∘ Bijection⇒Inverse diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda index d5e6b8e75d..2aaa1cdddd 100644 --- a/src/Function/Properties/Surjection.agda +++ b/src/Function/Properties/Surjection.agda @@ -45,11 +45,11 @@ mkSurjection f surjective = record ↠⇒⟶ = Surjection.function ↠⇒↪ : A ↠ B → B ↪ A -↠⇒↪ s = mk↪ {from = to} λ { ≡.refl → proj₂ (strictlySurjective _)} +↠⇒↪ s = mk↪ {from = to} λ { ≡.refl → to∘to⁻ _ } where open Surjection s ↠⇒⇔ : A ↠ B → A ⇔ B -↠⇒⇔ s = mk⇔ to (proj₁ ∘ surjective) +↠⇒⇔ s = mk⇔ to section where open Surjection s ------------------------------------------------------------------------ @@ -69,12 +69,12 @@ trans = Compose.surjection injective⇒to⁻-cong : (surj : Surjection S T) → (open Surjection surj) → Injective Eq₁._≈_ Eq₂._≈_ to → - Congruent Eq₂._≈_ Eq₁._≈_ to⁻ + Congruent Eq₂._≈_ Eq₁._≈_ section injective⇒to⁻-cong {T = T} surj injective {x} {y} x≈y = injective $ begin - to (to⁻ x) ≈⟨ to∘to⁻ x ⟩ - x ≈⟨ x≈y ⟩ - y ≈⟨ to∘to⁻ y ⟨ - to (to⁻ y) ∎ + to (section x) ≈⟨ to∘to⁻ x ⟩ + x ≈⟨ x≈y ⟩ + y ≈⟨ to∘to⁻ y ⟨ + to (section y) ∎ where open ≈-Reasoning T open Surjection surj diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index 9533cfb179..576e1b4a64 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -17,7 +17,7 @@ module Function.Structures {a b ℓ₁ ℓ₂} {B : Set b} (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain where -open import Data.Product.Base as Product using (∃; _×_; _,_) +open import Data.Product.Base as Product using (∃; _×_; _,_; proj₁; proj₂) open import Function.Base open import Function.Definitions open import Level using (_⊔_) @@ -69,6 +69,12 @@ record IsSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where strictlySurjective : StrictlySurjective _≈₂_ f strictlySurjective x = Product.map₂ (λ v → v Eq₁.refl) (surjective x) + section : B → A + section = proj₁ ∘ surjective + + section-inverseˡ : Inverseˡ _≈₁_ _≈₂_ f section + section-inverseˡ = λ y≈fx → (proj₂ ∘ surjective) _ y≈fx + record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field @@ -87,7 +93,7 @@ record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where } open IsSurjection isSurjection public - using (strictlySurjective) + using (strictlySurjective; section) ------------------------------------------------------------------------ From e42c6344df02ff31f1a6268622174d40eddef3cd Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 29 Jan 2025 10:29:22 +0000 Subject: [PATCH 02/64] DRY: delegate to `Function.Consequences` --- src/Function/Structures.agda | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index 576e1b4a64..4214a451f6 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -19,6 +19,7 @@ module Function.Structures {a b ℓ₁ ℓ₂} open import Data.Product.Base as Product using (∃; _×_; _,_; proj₁; proj₂) open import Function.Base +open import Function.Consequences open import Function.Definitions open import Level using (_⊔_) @@ -67,13 +68,16 @@ record IsSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where open IsCongruent isCongruent public strictlySurjective : StrictlySurjective _≈₂_ f - strictlySurjective x = Product.map₂ (λ v → v Eq₁.refl) (surjective x) + strictlySurjective = surjective⇒strictlySurjective _≈₂_ Eq₁.refl surjective section : B → A section = proj₁ ∘ surjective section-inverseˡ : Inverseˡ _≈₁_ _≈₂_ f section - section-inverseˡ = λ y≈fx → (proj₂ ∘ surjective) _ y≈fx + section-inverseˡ {x = x} = proj₂ (surjective x) + + section-strictInverseˡ : StrictlyInverseˡ _≈₂_ f section + section-strictInverseˡ _ = section-inverseˡ Eq₁.refl record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where @@ -110,12 +114,12 @@ record IsLeftInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ renaming (cong to to-cong) strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from - strictlyInverseˡ x = inverseˡ Eq₁.refl + strictlyInverseˡ = inverseˡ⇒strictlyInverseˡ _≈₁_ _≈₂_ Eq₁.refl inverseˡ isSurjection : IsSurjection to isSurjection = record { isCongruent = isCongruent - ; surjective = λ y → from y , inverseˡ + ; surjective = inverseˡ⇒surjective _≈₂_ inverseˡ } @@ -129,7 +133,7 @@ record IsRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ renaming (cong to to-cong) strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from - strictlyInverseʳ x = inverseʳ Eq₂.refl + strictlyInverseʳ = inverseʳ⇒strictlyInverseʳ _≈₁_ _≈₂_ Eq₂.refl inverseʳ record IsInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where From 9f86e57ece1834f2e78a1d8c379c3097f70436b9 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 29 Jan 2025 10:31:31 +0000 Subject: [PATCH 03/64] refactor: delegate systematically to `Consequences` and `Structures` --- src/Function/Bundles.agda | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index 4fe0f97529..54405f8155 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -25,7 +25,6 @@ import Function.Structures as FunctionStructures open import Level using (Level; _⊔_; suc) open import Data.Product.Base using (_,_; proj₁; proj₂) open import Relation.Binary.Bundles using (Setoid) -open import Relation.Binary.Core using (_Preserves_⟶_) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) import Relation.Binary.PropositionalEquality.Properties as ≡ @@ -114,17 +113,18 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where using ( strictlySurjective ; section + ; section-strictInverseˡ ) to⁻ : B → A - to⁻ = proj₁ ∘ surjective + to⁻ = section {-# WARNING_ON_USAGE to⁻ "Warning: to⁻ was deprecated in v2.3. Please use Function.Structures.IsSurjection.section instead. " #-} - to∘to⁻ : ∀ x → to (section x) ≈₂ x - to∘to⁻ = proj₂ ∘ strictlySurjective + to∘to⁻ : StrictlyInverseˡ _≈₂_ to section + to∘to⁻ = section-strictInverseˡ record Bijection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where @@ -227,6 +227,8 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where open IsLeftInverse isLeftInverse public using (module Eq₁; module Eq₂; strictlyInverseˡ; isSurjection) + open IsSurjection isSurjection public using (surjective) + equivalence : Equivalence equivalence = record { to-cong = to-cong @@ -243,7 +245,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where surjection = record { to = to ; cong = to-cong - ; surjective = λ y → from y , inverseˡ + ; surjective = surjective } @@ -253,7 +255,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where to : A → B from : B → A to-cong : Congruent _≈₁_ _≈₂_ to - from-cong : from Preserves _≈₂_ ⟶ _≈₁_ + from-cong : Congruent _≈₂_ _≈₁_ from inverseʳ : Inverseʳ _≈₁_ _≈₂_ to from isCongruent : IsCongruent to From 8ffbebf71211217c67395696d86b9e5d4c2b40e4 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 29 Jan 2025 10:47:08 +0000 Subject: [PATCH 04/64] add: `injective` and `isInjection` to `IsRightInverse` --- src/Function/Structures.agda | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index 4214a451f6..8fb9952e16 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -135,6 +135,15 @@ record IsRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from strictlyInverseʳ = inverseʳ⇒strictlyInverseʳ _≈₁_ _≈₂_ Eq₂.refl inverseʳ + injective : Injective _≈₁_ _≈₂_ to + injective = inverseʳ⇒injective {f⁻¹ = from} _≈₂_ to Eq₂.refl Eq₁.sym Eq₁.trans inverseʳ + + isInjection : IsInjection to + isInjection = record + { isCongruent = isCongruent + ; injective = injective + } + record IsInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field From 7ef3206f888a4ae9fe0c08f7c48e537c778cfea7 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 29 Jan 2025 10:52:58 +0000 Subject: [PATCH 05/64] add: `injection : Injection From To` to `IsRightInverse` --- src/Function/Bundles.agda | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index 54405f8155..87b4c53143 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -273,7 +273,9 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where } open IsRightInverse isRightInverse public - using (module Eq₁; module Eq₂; strictlyInverseʳ) + using (module Eq₁; module Eq₂; strictlyInverseʳ; isInjection) + + open IsInjection isInjection public using (injective) equivalence : Equivalence equivalence = record @@ -281,6 +283,13 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where ; from-cong = from-cong } + injection : Injection From To + injection = record + { to = to + ; cong = to-cong + ; injective = injective + } + record Inverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field From 2f6b3c2ebdd788adf3ecd16a7ca336c8d93f1629 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 29 Jan 2025 14:43:21 +0000 Subject: [PATCH 06/64] add: module `IsSurjective` to `Consequences` --- src/Function/Consequences.agda | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda index 2a13d452f6..e1ed9bcf4a 100644 --- a/src/Function/Consequences.agda +++ b/src/Function/Consequences.agda @@ -11,6 +11,7 @@ module Function.Consequences where open import Data.Product.Base as Product +open import Function.Base using (_∘_) open import Function.Definitions open import Level using (Level) open import Relation.Binary.Core using (Rel) @@ -81,6 +82,23 @@ strictlySurjective⇒surjective : Transitive ≈₂ → strictlySurjective⇒surjective trans cong surj x = Product.map₂ (λ fy≈x z≈y → trans (cong z≈y) fy≈x) (surj x) +module IsSurjective {f : A → B} (surjective : Surjective ≈₁ ≈₂ f) where + + section : B → A + section = proj₁ ∘ surjective + + section-inverseˡ : Inverseˡ ≈₁ ≈₂ f section + section-inverseˡ {x = x} = proj₂ (surjective x) + + module _ (refl : Reflexive ≈₁) where + + strictlySurjective : StrictlySurjective ≈₂ f + strictlySurjective = surjective⇒strictlySurjective ≈₂ refl surjective + + section-strictInverseˡ : StrictlyInverseˡ ≈₂ f section + section-strictInverseˡ _ = section-inverseˡ refl + + ------------------------------------------------------------------------ -- StrictlyInverseˡ From e6899efa93f87205d676e5766f787f71295f8cd3 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 29 Jan 2025 14:44:55 +0000 Subject: [PATCH 07/64] refactor: re-export from `Consequences.IsSurjective` --- src/Function/Structures.agda | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index 8fb9952e16..7de3e366c6 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -67,17 +67,16 @@ record IsSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where open IsCongruent isCongruent public - strictlySurjective : StrictlySurjective _≈₂_ f - strictlySurjective = surjective⇒strictlySurjective _≈₂_ Eq₁.refl surjective + private module IS = IsSurjective {≈₂ = _≈₂_} surjective - section : B → A - section = proj₁ ∘ surjective + open IS public + using (section; section-inverseˡ) - section-inverseˡ : Inverseˡ _≈₁_ _≈₂_ f section - section-inverseˡ {x = x} = proj₂ (surjective x) + strictlySurjective : StrictlySurjective _≈₂_ f + strictlySurjective = IS.strictlySurjective Eq₁.refl section-strictInverseˡ : StrictlyInverseˡ _≈₂_ f section - section-strictInverseˡ _ = section-inverseˡ Eq₁.refl + section-strictInverseˡ _ = IS.section-inverseˡ Eq₁.refl record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where @@ -97,7 +96,7 @@ record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where } open IsSurjection isSurjection public - using (strictlySurjective; section) + using (strictlySurjective; section; section-strictInverseˡ) ------------------------------------------------------------------------ From 3cd9e7b8c897beb19cc9d13211879ec664e2f663 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 29 Jan 2025 15:02:55 +0000 Subject: [PATCH 08/64] refactor: use module `IsSurjective` --- src/Function/Construct/Symmetry.agda | 31 +++++++++++++++++----------- 1 file changed, 19 insertions(+), 12 deletions(-) diff --git a/src/Function/Construct/Symmetry.agda b/src/Function/Construct/Symmetry.agda index 494197abbb..35475f4bd2 100644 --- a/src/Function/Construct/Symmetry.agda +++ b/src/Function/Construct/Symmetry.agda @@ -10,6 +10,8 @@ module Function.Construct.Symmetry where open import Data.Product.Base using (_,_; swap; proj₁; proj₂) open import Function.Base using (_∘_) +open import Function.Consequences + using (module IsSurjective) open import Function.Definitions using (Bijective; Injective; Surjective; Inverseˡ; Inverseʳ; Inverseᵇ; Congruent) open import Function.Structures @@ -35,21 +37,26 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} ((inj , surj) : Bijective ≈₁ ≈₂ f) where - private - f⁻¹ = proj₁ ∘ surj - f∘f⁻¹≡id = proj₂ ∘ surj + open IsSurjective {≈₂ = ≈₂} surj + using (section; section-strictInverseˡ) + + module _ (refl : Reflexive ≈₁) where + + private + + f∘section≡id = section-strictInverseˡ refl - injective : Reflexive ≈₁ → Symmetric ≈₂ → Transitive ≈₂ → - Congruent ≈₁ ≈₂ f → Injective ≈₂ ≈₁ f⁻¹ - injective refl sym trans cong gx≈gy = - trans (trans (sym (f∘f⁻¹≡id _ refl)) (cong gx≈gy)) (f∘f⁻¹≡id _ refl) + injective : Symmetric ≈₂ → Transitive ≈₂ → + Congruent ≈₁ ≈₂ f → Injective ≈₂ ≈₁ section + injective sym trans cong gx≈gy = + trans (trans (sym (f∘section≡id _)) (cong gx≈gy)) (f∘section≡id _) - surjective : Reflexive ≈₁ → Transitive ≈₂ → Surjective ≈₂ ≈₁ f⁻¹ - surjective refl trans x = f x , inj ∘ trans (f∘f⁻¹≡id _ refl) + surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ section + surjective trans x = f x , inj ∘ trans (f∘section≡id _) - bijective : Reflexive ≈₁ → Symmetric ≈₂ → Transitive ≈₂ → - Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ f⁻¹ - bijective refl sym trans cong = injective refl sym trans cong , surjective refl trans + bijective : Symmetric ≈₂ → Transitive ≈₂ → + Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ section + bijective sym trans cong = injective sym trans cong , surjective trans module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) {f : A → B} {f⁻¹ : B → A} where From eeb49e66a3acf5097e8c7ae545d9f7ef91be7830 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 29 Jan 2025 15:03:34 +0000 Subject: [PATCH 09/64] refactor: deprecate second definition --- src/Function/Bundles.agda | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index 87b4c53143..82889470b8 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -125,6 +125,10 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where to∘to⁻ : StrictlyInverseˡ _≈₂_ to section to∘to⁻ = section-strictInverseˡ + {-# WARNING_ON_USAGE to∘to⁻ + "Warning: to∘to⁻ was deprecated in v2.3. + Please use Function.Structures.IsSurjection.section-strictInverseˡ instead. " + #-} record Bijection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where From 520b838e390cedbaf5d661289d780c0bfe0e11ba Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 29 Jan 2025 15:26:14 +0000 Subject: [PATCH 10/64] =?UTF-8?q?refactor:=20deprecate=20`injective?= =?UTF-8?q?=E2=87=92to=E2=81=BB-cong`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Function/Properties/Surjection.agda | 23 +++++++++++++++++++---- 1 file changed, 19 insertions(+), 4 deletions(-) diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda index 2aaa1cdddd..081b30a69a 100644 --- a/src/Function/Properties/Surjection.agda +++ b/src/Function/Properties/Surjection.agda @@ -66,16 +66,31 @@ trans = Compose.surjection ------------------------------------------------------------------------ -- Other -injective⇒to⁻-cong : (surj : Surjection S T) → +injective⇒section-cong : (surj : Surjection S T) → (open Surjection surj) → Injective Eq₁._≈_ Eq₂._≈_ to → Congruent Eq₂._≈_ Eq₁._≈_ section -injective⇒to⁻-cong {T = T} surj injective {x} {y} x≈y = injective $ begin - to (section x) ≈⟨ to∘to⁻ x ⟩ +injective⇒section-cong {T = T} surj injective {x} {y} x≈y = injective $ begin + to (section x) ≈⟨ section-strictInverseˡ x ⟩ x ≈⟨ x≈y ⟩ - y ≈⟨ to∘to⁻ y ⟨ + y ≈⟨ section-strictInverseˡ y ⟨ to (section y) ∎ where open ≈-Reasoning T open Surjection surj + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.3 + +injective⇒to⁻-cong = injective⇒section-cong +{-# WARNING_ON_USAGE injective⇒to⁻-cong +"Warning: injective⇒to⁻-cong was deprecated in v2.3. +Please use injective⇒section-cong instead. " +#-} + From 8efb15d311e75bb0f9cd8897df7d54aaf4434f5e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 29 Jan 2025 16:14:28 +0000 Subject: [PATCH 11/64] fix: exports from `Surjection` and `Bijection` --- src/Function/Bundles.agda | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index 82889470b8..8b061513f8 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -113,6 +113,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where using ( strictlySurjective ; section + ; section-inverseˡ ; section-strictInverseˡ ) @@ -158,7 +159,12 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where open Injection injection public using (isInjection) open Surjection surjection public - using (isSurjection; section; to∘to⁻; strictlySurjective) + using (isSurjection + ; strictlySurjective + ; section + ; section-inverseˡ + ; section-strictInverseˡ + ) isBijection : IsBijection to isBijection = record From 576610f74cc45a872a13ada0bca1262355abea24 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 29 Jan 2025 16:15:49 +0000 Subject: [PATCH 12/64] =?UTF-8?q?refactor:=20deprecate=20`injective?= =?UTF-8?q?=E2=87=92to=E2=81=BB-cong`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Function/Properties/Surjection.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda index 081b30a69a..958a8ea585 100644 --- a/src/Function/Properties/Surjection.agda +++ b/src/Function/Properties/Surjection.agda @@ -93,4 +93,3 @@ injective⇒to⁻-cong = injective⇒section-cong "Warning: injective⇒to⁻-cong was deprecated in v2.3. Please use injective⇒section-cong instead. " #-} - From 08fb12279cec881719d33f34990717b24f162e2f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 29 Jan 2025 16:17:42 +0000 Subject: [PATCH 13/64] =?UTF-8?q?fix:=20symmetry=20of=20`Bijection`;=20dep?= =?UTF-8?q?recate=20`sym-=E2=89=A1`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Function/Properties/Bijection.agda | 65 ++++++++++++++++---------- 1 file changed, 41 insertions(+), 24 deletions(-) diff --git a/src/Function/Properties/Bijection.agda b/src/Function/Properties/Bijection.agda index 4219006ec0..3dca45e889 100644 --- a/src/Function/Properties/Bijection.agda +++ b/src/Function/Properties/Bijection.agda @@ -17,8 +17,9 @@ open import Relation.Binary.Definitions using (Reflexive; Trans) open import Relation.Binary.PropositionalEquality.Properties using (setoid) open import Data.Product.Base using (_,_; proj₁; proj₂) open import Function.Base using (_∘_) -open import Function.Properties.Surjection using (injective⇒to⁻-cong) -open import Function.Properties.Inverse using (Inverse⇒Equivalence) +open import Function.Properties.Surjection using (injective⇒section-cong) +open import Function.Properties.Inverse + using (Inverse⇒Bijection; Inverse⇒Equivalence) import Function.Construct.Identity as Identity import Function.Construct.Symmetry as Symmetry @@ -30,16 +31,33 @@ private A B : Set a T S : Setoid a ℓ +------------------------------------------------------------------------ +-- Conversion functions + +Bijection⇒Inverse : Bijection S T → Inverse S T +Bijection⇒Inverse bij = record + { to = to + ; from = section + ; to-cong = cong + ; from-cong = injective⇒section-cong surjection injective + ; inverse = section-inverseˡ + , λ y≈to[x] → injective (Eq₂.trans (section-strictInverseˡ _) y≈to[x]) + } + where open Bijection bij + +Bijection⇒Equivalence : Bijection T S → Equivalence T S +Bijection⇒Equivalence = Inverse⇒Equivalence ∘ Bijection⇒Inverse + ------------------------------------------------------------------------ -- Setoid properties refl : Reflexive (Bijection {a} {ℓ}) refl = Identity.bijection _ --- Can't prove full symmetry as we have no proof that the witness --- produced by the surjection proof preserves equality -sym-≡ : Bijection S (setoid B) → Bijection (setoid B) S -sym-≡ = Symmetry.bijection-≡ +-- Now we *can* prove full symmetry as we now have a proof that +-- the witness produced by the surjection proof preserves equality +sym : Bijection S T → Bijection T S +sym = Inverse⇒Bijection ∘ Symmetry.inverse ∘ Bijection⇒Inverse trans : Trans (Bijection {a} {ℓ₁} {b} {ℓ₂}) (Bijection {b} {ℓ₂} {c} {ℓ₃}) Bijection trans = Composition.bijection @@ -50,29 +68,28 @@ trans = Composition.bijection ⤖-isEquivalence : IsEquivalence {ℓ = ℓ} _⤖_ ⤖-isEquivalence = record { refl = refl - ; sym = sym-≡ + ; sym = sym ; trans = trans } ------------------------------------------------------------------------- --- Conversion functions - -Bijection⇒Inverse : Bijection S T → Inverse S T -Bijection⇒Inverse bij = record - { to = to - ; from = section - ; to-cong = cong - ; from-cong = injective⇒to⁻-cong surjection injective - ; inverse = (λ y≈to⁻[x] → Eq₂.trans (cong y≈to⁻[x]) (to∘to⁻ _)) , - (λ y≈to[x] → injective (Eq₂.trans (to∘to⁻ _) y≈to[x])) - } - where open Bijection bij - -Bijection⇒Equivalence : Bijection T S → Equivalence T S -Bijection⇒Equivalence = Inverse⇒Equivalence ∘ Bijection⇒Inverse - ⤖⇒↔ : A ⤖ B → A ↔ B ⤖⇒↔ = Bijection⇒Inverse ⤖⇒⇔ : A ⤖ B → A ⇔ B ⤖⇒⇔ = Bijection⇒Equivalence + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.3 + +sym-≡ : Bijection S (setoid B) → Bijection (setoid B) S +sym-≡ = Symmetry.bijection-≡ +{-# WARNING_ON_USAGE sym-≡ +"Warning: sym-≡ was deprecated in v2.3. +Please use sym instead. " +#-} From c15f74891b9d5e3f7a424b0404383ff75cd0455d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 29 Jan 2025 16:29:44 +0000 Subject: [PATCH 14/64] =?UTF-8?q?fix:=20deprecation=20via=20export=20of=20?= =?UTF-8?q?`sym-=E2=89=A1`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Function/Properties/Bijection.agda | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Function/Properties/Bijection.agda b/src/Function/Properties/Bijection.agda index 3dca45e889..229d522894 100644 --- a/src/Function/Properties/Bijection.agda +++ b/src/Function/Properties/Bijection.agda @@ -87,8 +87,9 @@ trans = Composition.bijection -- Version 2.3 -sym-≡ : Bijection S (setoid B) → Bijection (setoid B) S -sym-≡ = Symmetry.bijection-≡ +open Symmetry public + using () + renaming (bijection-≡ to sym-≡) {-# WARNING_ON_USAGE sym-≡ "Warning: sym-≡ was deprecated in v2.3. Please use sym instead. " From cf9c04ec106342903722025ba12b9e60c5172478 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 29 Jan 2025 18:36:54 +0000 Subject: [PATCH 15/64] fix: knock-ons --- .../Function/Dependent/Propositional.agda | 22 ++++--- .../Product/Function/Dependent/Setoid.agda | 65 ++++++++++--------- src/Function/Properties/Surjection.agda | 2 +- 3 files changed, 48 insertions(+), 41 deletions(-) diff --git a/src/Data/Product/Function/Dependent/Propositional.agda b/src/Data/Product/Function/Dependent/Propositional.agda index 8ec6cc8f9f..e39ec31bdc 100644 --- a/src/Data/Product/Function/Dependent/Propositional.agda +++ b/src/Data/Product/Function/Dependent/Propositional.agda @@ -194,17 +194,21 @@ module _ where to′ = map (to I↠J) (to A↠B) backcast : ∀ {i} → B i → B (to I↠J (section I↠J i)) - backcast = ≡.subst B (≡.sym (to∘to⁻ I↠J _)) + backcast = ≡.subst B (≡.sym (section-strictInverseˡ I↠J _)) - to⁻′ : Σ J B → Σ I A - to⁻′ = map (section I↠J) (Surjection.section A↠B ∘ backcast) + section′ : Σ J B → Σ I A + section′ = map (section I↠J) (section A↠B ∘ backcast) strictlySurjective′ : StrictlySurjective _≡_ to′ - strictlySurjective′ (x , y) = to⁻′ (x , y) , Σ-≡,≡→≡ - ( to∘to⁻ I↠J x - , (≡.subst B (to∘to⁻ I↠J x) (to A↠B (section A↠B (backcast y))) ≡⟨ ≡.cong (≡.subst B _) (to∘to⁻ A↠B _) ⟩ - ≡.subst B (to∘to⁻ I↠J x) (backcast y) ≡⟨ ≡.subst-subst-sym (to∘to⁻ I↠J x) ⟩ - y ∎) + strictlySurjective′ (x , y) = section′ (x , y) , Σ-≡,≡→≡ + ( section-strictInverseˡ I↠J x + , (begin + ≡.subst B (section-strictInverseˡ I↠J x) (to A↠B (section A↠B (backcast y))) + ≡⟨ ≡.cong (≡.subst B _) (section-strictInverseˡ A↠B _) ⟩ + ≡.subst B (section-strictInverseˡ I↠J x) (backcast y) + ≡⟨ ≡.subst-subst-sym (section-strictInverseˡ I↠J x) ⟩ + y + ∎) ) where open ≡.≡-Reasoning @@ -250,7 +254,7 @@ module _ where Σ-↔ {I = I} {J = J} {A = A} {B = B} I↔J A↔B = mk↔ₛ′ (Surjection.to surjection′) (Surjection.section surjection′) - (Surjection.to∘to⁻ surjection′) + (Surjection.section-strictInverseˡ surjection′) left-inverse-of where open ≡.≡-Reasoning diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda index 82442ac08f..f7f75e3c60 100644 --- a/src/Data/Product/Function/Dependent/Setoid.agda +++ b/src/Data/Product/Function/Dependent/Setoid.agda @@ -94,34 +94,37 @@ module _ where (function (⇔⇒⟶ I⇔J) A⟶B) (function (⇔⇒⟵ I⇔J) B⟶A) - equivalence-↪ : - (I↪J : I ↪ J) → - (∀ {i} → Equivalence (A atₛ (RightInverse.from I↪J i)) (B atₛ i)) → - Equivalence (I ×ₛ A) (J ×ₛ B) - equivalence-↪ {A = A} {B = B} I↪J A⇔B = - equivalence (RightInverse.equivalence I↪J) A→B (fromFunction A⇔B) - where - A→B : ∀ {i} → Func (A atₛ i) (B atₛ (RightInverse.to I↪J i)) - A→B = record - { to = to A⇔B ∘ cast A (RightInverse.strictlyInverseʳ I↪J _) - ; cong = to-cong A⇔B ∘ cast-cong A (RightInverse.strictlyInverseʳ I↪J _) - } - - equivalence-↠ : - (I↠J : I ↠ J) → - (∀ {x} → Equivalence (A atₛ x) (B atₛ (Surjection.to I↠J x))) → - Equivalence (I ×ₛ A) (J ×ₛ B) - equivalence-↠ {A = A} {B = B} I↠J A⇔B = - equivalence (↠⇒⇔ I↠J) B-to B-from - where - B-to : ∀ {x} → Func (A atₛ x) (B atₛ (Surjection.to I↠J x)) - B-to = toFunction A⇔B + module _ (I↪J : I ↪ J) where + + private module ItoJ = RightInverse I↪J + + equivalence-↪ : (∀ {i} → Equivalence (A atₛ (ItoJ.from i)) (B atₛ i)) → + Equivalence (I ×ₛ A) (J ×ₛ B) + equivalence-↪ {A = A} {B = B} A⇔B = + equivalence ItoJ.equivalence A→B (fromFunction A⇔B) + where + A→B : ∀ {i} → Func (A atₛ i) (B atₛ (ItoJ.to i)) + A→B = record + { to = to A⇔B ∘ cast A (ItoJ.strictlyInverseʳ _) + ; cong = to-cong A⇔B ∘ cast-cong A (ItoJ.strictlyInverseʳ _) + } + + module _ (I↠J : I ↠ J) where + + private module ItoJ = Surjection I↠J + + equivalence-↠ : (∀ {x} → Equivalence (A atₛ x) (B atₛ (ItoJ.to x))) → + Equivalence (I ×ₛ A) (J ×ₛ B) + equivalence-↠ {A = A} {B = B} A⇔B = equivalence (↠⇒⇔ I↠J) B-to B-from + where + B-to : ∀ {x} → Func (A atₛ x) (B atₛ (ItoJ.to x)) + B-to = toFunction A⇔B - B-from : ∀ {y} → Func (B atₛ y) (A atₛ (Surjection.section I↠J y)) - B-from = record - { to = from A⇔B ∘ cast B (Surjection.to∘to⁻ I↠J _) - ; cong = from-cong A⇔B ∘ cast-cong B (Surjection.to∘to⁻ I↠J _) - } + B-from : ∀ {y} → Func (B atₛ y) (A atₛ (ItoJ.section y)) + B-from = record + { to = from A⇔B ∘ cast B (ItoJ.section-strictInverseˡ _) + ; cong = from-cong A⇔B ∘ cast-cong B (ItoJ.section-strictInverseˡ _) + } ------------------------------------------------------------------------ -- Injections @@ -168,12 +171,12 @@ module _ where func : Func (I ×ₛ A) (J ×ₛ B) func = function (Surjection.function I↠J) (Surjection.function A↠B) - to⁻′ : Carrier (J ×ₛ B) → Carrier (I ×ₛ A) - to⁻′ (j , y) = section I↠J j , section A↠B (cast B (Surjection.to∘to⁻ I↠J _) y) + section′ : Carrier (J ×ₛ B) → Carrier (I ×ₛ A) + section′ (j , y) = section I↠J j , section A↠B (cast B (section-strictInverseˡ I↠J _) y) strictlySurj : StrictlySurjective (Func.Eq₂._≈_ func) (Func.to func) - strictlySurj (j , y) = to⁻′ (j , y) , - to∘to⁻ I↠J j , IndexedSetoid.trans B (to∘to⁻ A↠B _) (cast-eq B (to∘to⁻ I↠J j)) + strictlySurj (j , y) = section′ (j , y) , + section-strictInverseˡ I↠J j , IndexedSetoid.trans B (section-strictInverseˡ A↠B _) (cast-eq B (section-strictInverseˡ I↠J j)) surj : Surjective (Func.Eq₁._≈_ func) (Func.Eq₂._≈_ func) (Func.to func) surj = strictlySurjective⇒surjective (I ×ₛ A) (J ×ₛ B) (Func.cong func) strictlySurj diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda index 958a8ea585..e4b2b368aa 100644 --- a/src/Function/Properties/Surjection.agda +++ b/src/Function/Properties/Surjection.agda @@ -45,7 +45,7 @@ mkSurjection f surjective = record ↠⇒⟶ = Surjection.function ↠⇒↪ : A ↠ B → B ↪ A -↠⇒↪ s = mk↪ {from = to} λ { ≡.refl → to∘to⁻ _ } +↠⇒↪ s = mk↪ {from = to} λ { ≡.refl → section-strictInverseˡ _ } where open Surjection s ↠⇒⇔ : A ↠ B → A ⇔ B From f56cd9ee5f735e98aa1c3e86238d178235a8ef32 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 29 Jan 2025 18:38:19 +0000 Subject: [PATCH 16/64] fix: whitespace --- src/Data/Product/Function/Dependent/Setoid.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda index f7f75e3c60..32c52e5944 100644 --- a/src/Data/Product/Function/Dependent/Setoid.agda +++ b/src/Data/Product/Function/Dependent/Setoid.agda @@ -97,7 +97,7 @@ module _ where module _ (I↪J : I ↪ J) where private module ItoJ = RightInverse I↪J - + equivalence-↪ : (∀ {i} → Equivalence (A atₛ (ItoJ.from i)) (B atₛ i)) → Equivalence (I ×ₛ A) (J ×ₛ B) equivalence-↪ {A = A} {B = B} A⇔B = @@ -112,7 +112,7 @@ module _ where module _ (I↠J : I ↠ J) where private module ItoJ = Surjection I↠J - + equivalence-↠ : (∀ {x} → Equivalence (A atₛ x) (B atₛ (ItoJ.to x))) → Equivalence (I ×ₛ A) (J ×ₛ B) equivalence-↠ {A = A} {B = B} A⇔B = equivalence (↠⇒⇔ I↠J) B-to B-from From b855ebc6fc58d5ee662e00a63b7773294eb94171 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 29 Jan 2025 18:39:23 +0000 Subject: [PATCH 17/64] fix: indentation --- src/Function/Properties/Surjection.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda index e4b2b368aa..d3495dfd10 100644 --- a/src/Function/Properties/Surjection.agda +++ b/src/Function/Properties/Surjection.agda @@ -67,9 +67,9 @@ trans = Compose.surjection -- Other injective⇒section-cong : (surj : Surjection S T) → - (open Surjection surj) → - Injective Eq₁._≈_ Eq₂._≈_ to → - Congruent Eq₂._≈_ Eq₁._≈_ section + (open Surjection surj) → + Injective Eq₁._≈_ Eq₂._≈_ to → + Congruent Eq₂._≈_ Eq₁._≈_ section injective⇒section-cong {T = T} surj injective {x} {y} x≈y = injective $ begin to (section x) ≈⟨ section-strictInverseˡ x ⟩ x ≈⟨ x≈y ⟩ From 7fcbcb0ec253d5abf3b0a965863bd9ee59faa850 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 06:49:27 +0000 Subject: [PATCH 18/64] add: `section-cong` congruence proof --- src/Function/Construct/Symmetry.agda | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/Function/Construct/Symmetry.agda b/src/Function/Construct/Symmetry.agda index 35475f4bd2..a9cef2adf7 100644 --- a/src/Function/Construct/Symmetry.agda +++ b/src/Function/Construct/Symmetry.agda @@ -34,29 +34,29 @@ private -- Properties module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} - ((inj , surj) : Bijective ≈₁ ≈₂ f) + ((inj , surj) : Bijective ≈₁ ≈₂ f) (refl : Reflexive ≈₁) where open IsSurjective {≈₂ = ≈₂} surj using (section; section-strictInverseˡ) - module _ (refl : Reflexive ≈₁) where + private f∘section≡id = section-strictInverseˡ refl - private + section-cong : Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₂ ≈₁ section + section-cong sym trans = + inj ∘ trans (f∘section≡id _) ∘ sym ∘ trans (f∘section≡id _) ∘ sym - f∘section≡id = section-strictInverseˡ refl + injective : Symmetric ≈₂ → Transitive ≈₂ → + Congruent ≈₁ ≈₂ f → Injective ≈₂ ≈₁ section + injective sym trans cong gx≈gy = + trans (trans (sym (f∘section≡id _)) (cong gx≈gy)) (f∘section≡id _) - injective : Symmetric ≈₂ → Transitive ≈₂ → - Congruent ≈₁ ≈₂ f → Injective ≈₂ ≈₁ section - injective sym trans cong gx≈gy = - trans (trans (sym (f∘section≡id _)) (cong gx≈gy)) (f∘section≡id _) + surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ section + surjective trans x = f x , inj ∘ trans (f∘section≡id _) - surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ section - surjective trans x = f x , inj ∘ trans (f∘section≡id _) - - bijective : Symmetric ≈₂ → Transitive ≈₂ → + bijective : Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ section - bijective sym trans cong = injective sym trans cong , surjective trans + bijective sym trans cong = injective sym trans cong , surjective trans module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) {f : A → B} {f⁻¹ : B → A} where From fbc5c5036d1a737ae0b1f3ff0a2d1a6f07c96b11 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 06:57:55 +0000 Subject: [PATCH 19/64] =?UTF-8?q?refactor:=20deprecate=20`injective?= =?UTF-8?q?=E2=87=92to=E2=81=BB-cong`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Function/Properties/Surjection.agda | 38 ++++++++++--------------- 1 file changed, 15 insertions(+), 23 deletions(-) diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda index d3495dfd10..bd34c3966e 100644 --- a/src/Function/Properties/Surjection.agda +++ b/src/Function/Properties/Surjection.agda @@ -10,12 +10,13 @@ module Function.Properties.Surjection where open import Function.Base using (_∘_; _$_) open import Function.Definitions using (Surjective; Injective; Congruent) -open import Function.Bundles using (Func; Surjection; _↠_; _⟶_; _↪_; mk↪; - _⇔_; mk⇔) +open import Function.Bundles + using (Func; Surjection; _↠_; _⟶_; _↪_; mk↪; _⇔_; mk⇔) import Function.Construct.Identity as Identity +import Function.Construct.Symmetry as Symmetry import Function.Construct.Composition as Compose open import Level using (Level) -open import Data.Product.Base using (proj₁; proj₂) +open import Data.Product.Base using (_,_; proj₁; proj₂) import Relation.Binary.PropositionalEquality.Core as ≡ open import Relation.Binary.Definitions using (Reflexive; Trans) open import Relation.Binary.Bundles using (Setoid) @@ -31,8 +32,8 @@ private -- Constructors mkSurjection : (f : Func S T) (open Func f) → - Surjective Eq₁._≈_ Eq₂._≈_ to → - Surjection S T + Surjective Eq₁._≈_ Eq₂._≈_ to → + Surjection S T mkSurjection f surjective = record { Func f ; surjective = surjective @@ -63,22 +64,6 @@ trans : Trans (Surjection {a} {ℓ₁} {b} {ℓ₂}) (Surjection {a} {ℓ₁} {c} {ℓ₃}) trans = Compose.surjection ------------------------------------------------------------------------- --- Other - -injective⇒section-cong : (surj : Surjection S T) → - (open Surjection surj) → - Injective Eq₁._≈_ Eq₂._≈_ to → - Congruent Eq₂._≈_ Eq₁._≈_ section -injective⇒section-cong {T = T} surj injective {x} {y} x≈y = injective $ begin - to (section x) ≈⟨ section-strictInverseˡ x ⟩ - x ≈⟨ x≈y ⟩ - y ≈⟨ section-strictInverseˡ y ⟨ - to (section y) ∎ - where - open ≈-Reasoning T - open Surjection surj - ------------------------------------------------------------------------ -- DEPRECATED NAMES @@ -88,8 +73,15 @@ injective⇒section-cong {T = T} surj injective {x} {y} x≈y = injective $ begi -- Version 2.3 -injective⇒to⁻-cong = injective⇒section-cong +module _ (surjection : Surjection S T) where + + open Surjection surjection + + injective⇒to⁻-cong : Injective Eq₁._≈_ Eq₂._≈_ to → + Congruent Eq₂._≈_ Eq₁._≈_ section + injective⇒to⁻-cong injective = + Symmetry.section-cong (injective , surjective) Eq₁.refl Eq₂.sym Eq₂.trans {-# WARNING_ON_USAGE injective⇒to⁻-cong "Warning: injective⇒to⁻-cong was deprecated in v2.3. -Please use injective⇒section-cong instead. " +Please use Symmetry.section-cong instead. " #-} From 68e58cf1af9c0e9a16a8763587ec3e886e7a1cf6 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 07:02:31 +0000 Subject: [PATCH 20/64] fix: whitespace --- src/Function/Properties/Surjection.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda index bd34c3966e..4076d25a1a 100644 --- a/src/Function/Properties/Surjection.agda +++ b/src/Function/Properties/Surjection.agda @@ -76,7 +76,7 @@ trans = Compose.surjection module _ (surjection : Surjection S T) where open Surjection surjection - + injective⇒to⁻-cong : Injective Eq₁._≈_ Eq₂._≈_ to → Congruent Eq₂._≈_ Eq₁._≈_ section injective⇒to⁻-cong injective = From 6bb39ce4dda711daf536825447d8353d5bed2e4b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 07:10:46 +0000 Subject: [PATCH 21/64] refactor: use `section-cong` --- src/Function/Properties/Bijection.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Function/Properties/Bijection.agda b/src/Function/Properties/Bijection.agda index 229d522894..eabcbdca0b 100644 --- a/src/Function/Properties/Bijection.agda +++ b/src/Function/Properties/Bijection.agda @@ -17,7 +17,6 @@ open import Relation.Binary.Definitions using (Reflexive; Trans) open import Relation.Binary.PropositionalEquality.Properties using (setoid) open import Data.Product.Base using (_,_; proj₁; proj₂) open import Function.Base using (_∘_) -open import Function.Properties.Surjection using (injective⇒section-cong) open import Function.Properties.Inverse using (Inverse⇒Bijection; Inverse⇒Equivalence) @@ -39,7 +38,7 @@ Bijection⇒Inverse bij = record { to = to ; from = section ; to-cong = cong - ; from-cong = injective⇒section-cong surjection injective + ; from-cong = Symmetry.section-cong bijective Eq₁.refl Eq₂.sym Eq₂.trans ; inverse = section-inverseˡ , λ y≈to[x] → injective (Eq₂.trans (section-strictInverseˡ _) y≈to[x]) } From 72f7c7875c990cf1a207fb984995fbc857bb4582 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 10:36:33 +0000 Subject: [PATCH 22/64] refactor: move properties from `Symmetry` to `Consequences`; rename module --- src/Function/Consequences.agda | 52 +++++++++++++++++++++++----------- 1 file changed, 35 insertions(+), 17 deletions(-) diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda index e1ed9bcf4a..e79e7daa4f 100644 --- a/src/Function/Consequences.agda +++ b/src/Function/Consequences.agda @@ -82,23 +82,6 @@ strictlySurjective⇒surjective : Transitive ≈₂ → strictlySurjective⇒surjective trans cong surj x = Product.map₂ (λ fy≈x z≈y → trans (cong z≈y) fy≈x) (surj x) -module IsSurjective {f : A → B} (surjective : Surjective ≈₁ ≈₂ f) where - - section : B → A - section = proj₁ ∘ surjective - - section-inverseˡ : Inverseˡ ≈₁ ≈₂ f section - section-inverseˡ {x = x} = proj₂ (surjective x) - - module _ (refl : Reflexive ≈₁) where - - strictlySurjective : StrictlySurjective ≈₂ f - strictlySurjective = surjective⇒strictlySurjective ≈₂ refl surjective - - section-strictInverseˡ : StrictlyInverseˡ ≈₂ f section - section-strictInverseˡ _ = section-inverseˡ refl - - ------------------------------------------------------------------------ -- StrictlyInverseˡ @@ -130,3 +113,38 @@ strictlyInverseʳ⇒inverseʳ : Transitive ≈₁ → Inverseʳ ≈₁ ≈₂ f f⁻¹ strictlyInverseʳ⇒inverseʳ trans cong sinv {x} y≈f⁻¹x = trans (cong y≈f⁻¹x) (sinv x) + +------------------------------------------------------------------------ +-- Theory of the section of a Surjective function + +module Section (≈₂ : Rel B ℓ₂) (surj : Surjective {A = A} ≈₁ ≈₂ f) where + + section : B → A + section = proj₁ ∘ surj + + inverseˡ : Inverseˡ ≈₁ ≈₂ f section + inverseˡ {x = x} = proj₂ (surj x) + + module _ (refl : Reflexive ≈₁) where + + strictlySurjective : StrictlySurjective ≈₂ f + strictlySurjective = surjective⇒strictlySurjective ≈₂ refl surj + + strictInverseˡ : StrictlyInverseˡ ≈₂ f section + strictInverseˡ _ = inverseˡ refl + + module _ (inj : Injective ≈₁ ≈₂ f) (refl : Reflexive ≈₁) where + + private f∘section≡id = strictInverseˡ refl + + cong : Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₂ ≈₁ section + cong sym trans = inj ∘ trans (f∘section≡id _) ∘ sym ∘ trans (f∘section≡id _) ∘ sym + + surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ section + surjective trans x = f x , inj ∘ trans (f∘section≡id _) + + injective : Symmetric ≈₂ → Transitive ≈₂ → Injective ≈₂ ≈₁ section + injective sym trans = trans (sym (f∘section≡id _)) ∘ inverseˡ + + bijective : Symmetric ≈₂ → Transitive ≈₂ → Bijective ≈₂ ≈₁ section + bijective sym trans = injective sym trans , surjective trans From 2bcad3b6f331e08cc70c053d9dbf7c69b39823c0 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 11:10:05 +0000 Subject: [PATCH 23/64] refactor: sharpen sub-module parameterisation --- src/Function/Consequences.agda | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda index e79e7daa4f..83dc214ce3 100644 --- a/src/Function/Consequences.agda +++ b/src/Function/Consequences.agda @@ -130,12 +130,15 @@ module Section (≈₂ : Rel B ℓ₂) (surj : Surjective {A = A} ≈₁ ≈₂ strictlySurjective : StrictlySurjective ≈₂ f strictlySurjective = surjective⇒strictlySurjective ≈₂ refl surj - strictInverseˡ : StrictlyInverseˡ ≈₂ f section - strictInverseˡ _ = inverseˡ refl + strictlyInverseˡ : StrictlyInverseˡ ≈₂ f section + strictlyInverseˡ _ = inverseˡ refl + + injective : Symmetric ≈₂ → Transitive ≈₂ → Injective ≈₂ ≈₁ section + injective sym trans = trans (sym (strictlyInverseˡ _)) ∘ inverseˡ module _ (inj : Injective ≈₁ ≈₂ f) (refl : Reflexive ≈₁) where - private f∘section≡id = strictInverseˡ refl + private f∘section≡id = strictlyInverseˡ refl cong : Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₂ ≈₁ section cong sym trans = inj ∘ trans (f∘section≡id _) ∘ sym ∘ trans (f∘section≡id _) ∘ sym @@ -143,8 +146,5 @@ module Section (≈₂ : Rel B ℓ₂) (surj : Surjective {A = A} ≈₁ ≈₂ surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ section surjective trans x = f x , inj ∘ trans (f∘section≡id _) - injective : Symmetric ≈₂ → Transitive ≈₂ → Injective ≈₂ ≈₁ section - injective sym trans = trans (sym (f∘section≡id _)) ∘ inverseˡ - bijective : Symmetric ≈₂ → Transitive ≈₂ → Bijective ≈₂ ≈₁ section - bijective sym trans = injective sym trans , surjective trans + bijective sym trans = injective refl sym trans , surjective trans From 6d725fd20344452eff37bb564a58a222f80c6419 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 12:39:07 +0000 Subject: [PATCH 24/64] refactor: use module ; rectify exported names --- src/Function/Structures.agda | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index 7de3e366c6..f836b17ec1 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -67,16 +67,15 @@ record IsSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where open IsCongruent isCongruent public - private module IS = IsSurjective {≈₂ = _≈₂_} surjective + private module S = Section _≈₂_ surjective - open IS public - using (section; section-inverseˡ) + open S public using (section; inverseˡ) strictlySurjective : StrictlySurjective _≈₂_ f - strictlySurjective = IS.strictlySurjective Eq₁.refl + strictlySurjective = S.strictlySurjective Eq₁.refl - section-strictInverseˡ : StrictlyInverseˡ _≈₂_ f section - section-strictInverseˡ _ = IS.section-inverseˡ Eq₁.refl + strictlyInverseˡ : StrictlyInverseˡ _≈₂_ f section + strictlyInverseˡ _ = S.inverseˡ Eq₁.refl record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where @@ -96,7 +95,7 @@ record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where } open IsSurjection isSurjection public - using (strictlySurjective; section; section-strictInverseˡ) + using (strictlySurjective; section; inverseˡ; strictlyInverseˡ) ------------------------------------------------------------------------ From dfce04f6d29f0e63510524f1b04f1905bad3aa15 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 12:39:47 +0000 Subject: [PATCH 25/64] refactor: use module ; rectify exported names --- src/Function/Bundles.agda | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index 8b061513f8..f8a51d2412 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -113,8 +113,8 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where using ( strictlySurjective ; section - ; section-inverseˡ - ; section-strictInverseˡ + ; inverseˡ + ; strictlyInverseˡ ) to⁻ : B → A @@ -125,10 +125,10 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where #-} to∘to⁻ : StrictlyInverseˡ _≈₂_ to section - to∘to⁻ = section-strictInverseˡ + to∘to⁻ = strictlyInverseˡ {-# WARNING_ON_USAGE to∘to⁻ "Warning: to∘to⁻ was deprecated in v2.3. - Please use Function.Structures.IsSurjection.section-strictInverseˡ instead. " + Please use Function.Structures.IsSurjection.strictlyInverseˡ instead. " #-} @@ -162,8 +162,8 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where using (isSurjection ; strictlySurjective ; section - ; section-inverseˡ - ; section-strictInverseˡ + ; inverseˡ + ; strictlyInverseˡ ) isBijection : IsBijection to From b35b5a11fb4342bc412bbfcece8dd55b6e9bde37 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 12:41:03 +0000 Subject: [PATCH 26/64] refactor: fix names, deprecations for v2.3 --- src/Function/Construct/Symmetry.agda | 153 +++++++++++++++------------ 1 file changed, 87 insertions(+), 66 deletions(-) diff --git a/src/Function/Construct/Symmetry.agda b/src/Function/Construct/Symmetry.agda index a9cef2adf7..b4b397ac78 100644 --- a/src/Function/Construct/Symmetry.agda +++ b/src/Function/Construct/Symmetry.agda @@ -11,7 +11,7 @@ module Function.Construct.Symmetry where open import Data.Product.Base using (_,_; swap; proj₁; proj₂) open import Function.Base using (_∘_) open import Function.Consequences - using (module IsSurjective) + using (module Section) open import Function.Definitions using (Bijective; Injective; Surjective; Inverseˡ; Inverseʳ; Inverseᵇ; Congruent) open import Function.Structures @@ -33,31 +33,6 @@ private ------------------------------------------------------------------------ -- Properties -module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} - ((inj , surj) : Bijective ≈₁ ≈₂ f) (refl : Reflexive ≈₁) - where - - open IsSurjective {≈₂ = ≈₂} surj - using (section; section-strictInverseˡ) - - private f∘section≡id = section-strictInverseˡ refl - - section-cong : Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₂ ≈₁ section - section-cong sym trans = - inj ∘ trans (f∘section≡id _) ∘ sym ∘ trans (f∘section≡id _) ∘ sym - - injective : Symmetric ≈₂ → Transitive ≈₂ → - Congruent ≈₁ ≈₂ f → Injective ≈₂ ≈₁ section - injective sym trans cong gx≈gy = - trans (trans (sym (f∘section≡id _)) (cong gx≈gy)) (f∘section≡id _) - - surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ section - surjective trans x = f x , inj ∘ trans (f∘section≡id _) - - bijective : Symmetric ≈₂ → Transitive ≈₂ → - Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ section - bijective sym trans cong = injective sym trans cong , surjective trans - module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) {f : A → B} {f⁻¹ : B → A} where inverseʳ : Inverseˡ ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₂ ≈₁ f⁻¹ f @@ -76,31 +51,22 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} (isBij : IsBijection ≈₁ ≈₂ f) where - private - module IB = IsBijection isBij + private module B = IsBijection isBij - -- We can only flip a bijection if the witness produced by the - -- surjection proof respects the equality on the codomain. - isBijection : Congruent ≈₂ ≈₁ IB.section → IsBijection ≈₂ ≈₁ IB.section - isBijection section-cong = record + -- We can ALWAYS flip a bijection, WITHOUT knowing the witness produced + -- by the surjection proof respects the equality on the codomain. + isBijectionWithoutCongruence : IsBijection ≈₂ ≈₁ B.section + isBijectionWithoutCongruence = record { isInjection = record { isCongruent = record - { cong = section-cong - ; isEquivalence₁ = IB.Eq₂.isEquivalence - ; isEquivalence₂ = IB.Eq₁.isEquivalence + { cong = S.cong B.injective B.Eq₁.refl B.Eq₂.sym B.Eq₂.trans + ; isEquivalence₁ = B.Eq₂.isEquivalence + ; isEquivalence₂ = B.Eq₁.isEquivalence } - ; injective = injective IB.bijective IB.Eq₁.refl IB.Eq₂.sym IB.Eq₂.trans IB.cong + ; injective = S.injective B.Eq₁.refl B.Eq₂.sym B.Eq₂.trans } - ; surjective = surjective IB.bijective IB.Eq₁.refl IB.Eq₂.trans - } - -module _ {≈₁ : Rel A ℓ₁} {f : A → B} (isBij : IsBijection ≈₁ _≡_ f) where - - -- We can always flip a bijection if using the equality over the - -- codomain is propositional equality. - isBijection-≡ : IsBijection _≡_ ≈₁ _ - isBijection-≡ = isBijection isBij (IB.Eq₁.reflexive ∘ cong IB.section) - where module IB = IsBijection isBij + ; surjective = S.surjective B.injective B.Eq₁.refl B.Eq₂.trans + } where module S = Section ≈₂ B.surjective module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} {f⁻¹ : B → A} where @@ -136,24 +102,14 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} {f⁻¹ : module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} (bij : Bijection R S) where - private - module IB = Bijection bij - - -- We can only flip a bijection if the witness produced by the - -- surjection proof respects the equality on the codomain. - bijection : Congruent IB.Eq₂._≈_ IB.Eq₁._≈_ IB.section → Bijection S R - bijection cong = record - { to = IB.section - ; cong = cong - ; bijective = bijective IB.bijective IB.Eq₁.refl IB.Eq₂.sym IB.Eq₂.trans IB.cong - } - --- We can always flip a bijection if using the equality over the --- codomain is propositional equality. -bijection-≡ : {R : Setoid a ℓ₁} {B : Set b} → - Bijection R (setoid B) → Bijection (setoid B) R -bijection-≡ bij = bijection bij (B.Eq₁.reflexive ∘ cong _) - where module B = Bijection bij + -- We can always flip a bijection WITHOUT knowing if the witness produced + -- by the surjection proof respects the equality on the codomain. + bijectionWithoutCongruence : Bijection S R + bijectionWithoutCongruence = record + { to = B.section + ; cong = S.cong B.injective B.Eq₁.refl B.Eq₂.sym B.Eq₂.trans + ; bijective = S.bijective B.injective B.Eq₁.refl B.Eq₂.sym B.Eq₂.trans + } where module B = Bijection bij ; module S = Section (Setoid._≈_ S) B.surjective module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} where @@ -196,7 +152,7 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} where -- Propositional bundles ⤖-sym : A ⤖ B → B ⤖ A -⤖-sym b = bijection b (cong section) where open Bijection b using (section) +⤖-sym = bijectionWithoutCongruence ⇔-sym : A ⇔ B → B ⇔ A ⇔-sym = equivalence @@ -217,7 +173,7 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} where -- Please use the new names as continuing support for the old names is -- not guaranteed. --- Version v2.0 +-- Version 2.0 sym-⤖ = ⤖-sym {-# WARNING_ON_USAGE sym-⤖ @@ -248,3 +204,68 @@ sym-↔ = ↔-sym "Warning: sym-↔ was deprecated in v2.0. Please use ↔-sym instead." #-} + +-- Version 2.3 + +module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} + ((inj , surj) : Bijective ≈₁ ≈₂ f) (refl : Reflexive ≈₁) + where + + private + module S = Section ≈₂ surj + + injective : Symmetric ≈₂ → Transitive ≈₂ → + Congruent ≈₁ ≈₂ f → Injective ≈₂ ≈₁ S.section + injective sym trans _ = S.injective refl sym trans + + surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ S.section + surjective = S.surjective inj refl + + bijective : Symmetric ≈₂ → Transitive ≈₂ → + Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ S.section + bijective sym trans _ = S.injective refl sym trans , surjective trans +{-# WARNING_ON_USAGE injective +"Warning: injective was deprecated in v2.0. +Please use Function.Consequences.Section.injective instead, with a sharper type." +#-} +{-# WARNING_ON_USAGE surjective +"Warning: surjective was deprecated in v2.0. +Please use Function.Consequences.Section.surjective instead." +#-} +{-# WARNING_ON_USAGE bijective +"Warning: bijective was deprecated in v2.0. +Please use Function.Consequences.Section.bijective instead, with a sharper type." +#-} + +module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} + {f : A → B} (isBij : IsBijection ≈₁ ≈₂ f) + where + private module B = IsBijection isBij + isBijection : Congruent ≈₂ ≈₁ B.section → IsBijection ≈₂ ≈₁ B.section + isBijection _ = isBijectionWithoutCongruence isBij +{-# WARNING_ON_USAGE isBijection +"Warning: isBijection was deprecated in v2.3. +Please use isBijectionWithoutCongruence instead, with a sharper type." +#-} + +module _ {≈₁ : Rel A ℓ₁} {f : A → B} (isBij : IsBijection ≈₁ _≡_ f) where + isBijection-≡ : IsBijection _≡_ ≈₁ _ + isBijection-≡ = isBijectionWithoutCongruence isBij +{-# WARNING_ON_USAGE isBijection-≡ +"Warning: isBijection-≡ was deprecated in v2.3. +Please use isBijectionWithoutCongruence instead, with a sharper type." +#-} + +module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} (bij : Bijection R S) where + private module B = Bijection bij + bijection : Congruent B.Eq₂._≈_ B.Eq₁._≈_ B.section → Bijection S R + bijection _ = bijectionWithoutCongruence bij + +bijection-≡ : {R : Setoid a ℓ₁} {B : Set b} → + Bijection R (setoid B) → Bijection (setoid B) R +bijection-≡ = bijectionWithoutCongruence +{-# WARNING_ON_USAGE bijection-≡ +"Warning: bijection-≡ was deprecated in v2.3. +Please use bijectionWithoutCongruence instead, with a sharper type." +#-} + From ace7b086062f7f47aafef3ab5ea2da161dec6b0f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 13:28:58 +0000 Subject: [PATCH 27/64] =?UTF-8?q?refactor:=20lift=20out=20`inverse=CA=B3`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Function/Consequences.agda | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda index 83dc214ce3..f54e2a873a 100644 --- a/src/Function/Consequences.agda +++ b/src/Function/Consequences.agda @@ -143,8 +143,11 @@ module Section (≈₂ : Rel B ℓ₂) (surj : Surjective {A = A} ≈₁ ≈₂ cong : Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₂ ≈₁ section cong sym trans = inj ∘ trans (f∘section≡id _) ∘ sym ∘ trans (f∘section≡id _) ∘ sym + inverseʳ : Transitive ≈₂ → Inverseʳ ≈₁ ≈₂ f section + inverseʳ trans = inj ∘ trans (f∘section≡id _) + surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ section - surjective trans x = f x , inj ∘ trans (f∘section≡id _) + surjective trans x = f x , inverseʳ trans bijective : Symmetric ≈₂ → Transitive ≈₂ → Bijective ≈₂ ≈₁ section bijective sym trans = injective refl sym trans , surjective trans From f12d36ff421086f773fbee5f688d0577983cf944 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 13:45:36 +0000 Subject: [PATCH 28/64] =?UTF-8?q?refactor:=20lift=20out=20`strictlyInverse?= =?UTF-8?q?=CA=B3`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Function/Consequences.agda | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda index f54e2a873a..70ab1983ea 100644 --- a/src/Function/Consequences.agda +++ b/src/Function/Consequences.agda @@ -146,6 +146,9 @@ module Section (≈₂ : Rel B ℓ₂) (surj : Surjective {A = A} ≈₁ ≈₂ inverseʳ : Transitive ≈₂ → Inverseʳ ≈₁ ≈₂ f section inverseʳ trans = inj ∘ trans (f∘section≡id _) + strictlyInverseʳ : Transitive ≈₂ → {!StrictlyInverseʳ ≈₂ section f!} + strictlyInverseʳ trans = inverseʳ⇒strictlyInverseʳ ≈₂ ≈₁ refl inverseˡ + surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ section surjective trans x = f x , inverseʳ trans From 143988784120eed66e0962ee137091436b526f6a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 13:45:51 +0000 Subject: [PATCH 29/64] =?UTF-8?q?refactor:=20lift=20out=20`strictlyInverse?= =?UTF-8?q?=CA=B3`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Function/Consequences.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda index 70ab1983ea..70f0a26f85 100644 --- a/src/Function/Consequences.agda +++ b/src/Function/Consequences.agda @@ -146,7 +146,7 @@ module Section (≈₂ : Rel B ℓ₂) (surj : Surjective {A = A} ≈₁ ≈₂ inverseʳ : Transitive ≈₂ → Inverseʳ ≈₁ ≈₂ f section inverseʳ trans = inj ∘ trans (f∘section≡id _) - strictlyInverseʳ : Transitive ≈₂ → {!StrictlyInverseʳ ≈₂ section f!} + strictlyInverseʳ : Transitive ≈₂ → StrictlyInverseʳ ≈₂ section f strictlyInverseʳ trans = inverseʳ⇒strictlyInverseʳ ≈₂ ≈₁ refl inverseˡ surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ section From 53ab09aa0c63d5f06b59b7f23b1d09a29cfabdd7 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 13:51:59 +0000 Subject: [PATCH 30/64] refactor: propagate exports of new lemmas --- src/Function/Bundles.agda | 3 ++- src/Function/Structures.agda | 8 ++++++++ 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index f8a51d2412..926b636c93 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -172,7 +172,8 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where ; surjective = surjective } - open IsBijection isBijection public using (module Eq₁; module Eq₂) + open IsBijection isBijection public + using (module Eq₁; module Eq₂; inverseʳ; strictlyInverseʳ) ------------------------------------------------------------------------ diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index f836b17ec1..a70ef113e3 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -97,6 +97,14 @@ record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where open IsSurjection isSurjection public using (strictlySurjective; section; inverseˡ; strictlyInverseˡ) + private module S = Section _≈₂_ surjective + + inverseʳ : Inverseʳ _≈₁_ _≈₂_ f section + inverseʳ = S.inverseʳ injective Eq₁.refl Eq₂.trans + + strictlyInverseʳ : StrictlyInverseʳ _≈₂_ section f + strictlyInverseʳ = S.strictlyInverseʳ injective Eq₁.refl Eq₂.trans + ------------------------------------------------------------------------ -- Two element structures From 9070bfd2ecf7318c309a8fcd32944746175c6e95 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 13:53:13 +0000 Subject: [PATCH 31/64] =?UTF-8?q?refactor:=20clean=20up=20`Bijection?= =?UTF-8?q?=E2=87=92Inverse`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Function/Properties/Bijection.agda | 36 +++++++++++++------------- 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/src/Function/Properties/Bijection.agda b/src/Function/Properties/Bijection.agda index eabcbdca0b..ca560f77bd 100644 --- a/src/Function/Properties/Bijection.agda +++ b/src/Function/Properties/Bijection.agda @@ -30,23 +30,6 @@ private A B : Set a T S : Setoid a ℓ ------------------------------------------------------------------------- --- Conversion functions - -Bijection⇒Inverse : Bijection S T → Inverse S T -Bijection⇒Inverse bij = record - { to = to - ; from = section - ; to-cong = cong - ; from-cong = Symmetry.section-cong bijective Eq₁.refl Eq₂.sym Eq₂.trans - ; inverse = section-inverseˡ - , λ y≈to[x] → injective (Eq₂.trans (section-strictInverseˡ _) y≈to[x]) - } - where open Bijection bij - -Bijection⇒Equivalence : Bijection T S → Equivalence T S -Bijection⇒Equivalence = Inverse⇒Equivalence ∘ Bijection⇒Inverse - ------------------------------------------------------------------------ -- Setoid properties @@ -56,11 +39,28 @@ refl = Identity.bijection _ -- Now we *can* prove full symmetry as we now have a proof that -- the witness produced by the surjection proof preserves equality sym : Bijection S T → Bijection T S -sym = Inverse⇒Bijection ∘ Symmetry.inverse ∘ Bijection⇒Inverse +sym = Symmetry.bijectionWithoutCongruence trans : Trans (Bijection {a} {ℓ₁} {b} {ℓ₂}) (Bijection {b} {ℓ₂} {c} {ℓ₃}) Bijection trans = Composition.bijection +------------------------------------------------------------------------ +-- Conversion functions + +Bijection⇒Inverse : Bijection S T → Inverse S T +Bijection⇒Inverse bij = record + { to = to + ; from = Bijection.to (sym bij) + ; to-cong = cong + ; from-cong = Bijection.cong (sym bij) + ; inverse = inverseˡ , inverseʳ + + } + where open Bijection bij + +Bijection⇒Equivalence : Bijection T S → Equivalence T S +Bijection⇒Equivalence = Inverse⇒Equivalence ∘ Bijection⇒Inverse + ------------------------------------------------------------------------ -- Propositional properties From 9d1bd5ef99471064b4ab0433f9dcff8b11b691bd Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 14:04:32 +0000 Subject: [PATCH 32/64] fix: deprecated definition --- src/Function/Properties/Surjection.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda index 4076d25a1a..d5dcf297fc 100644 --- a/src/Function/Properties/Surjection.agda +++ b/src/Function/Properties/Surjection.agda @@ -12,8 +12,8 @@ open import Function.Base using (_∘_; _$_) open import Function.Definitions using (Surjective; Injective; Congruent) open import Function.Bundles using (Func; Surjection; _↠_; _⟶_; _↪_; mk↪; _⇔_; mk⇔) +open import Function.Consequences using (module Section) import Function.Construct.Identity as Identity -import Function.Construct.Symmetry as Symmetry import Function.Construct.Composition as Compose open import Level using (Level) open import Data.Product.Base using (_,_; proj₁; proj₂) @@ -46,7 +46,7 @@ mkSurjection f surjective = record ↠⇒⟶ = Surjection.function ↠⇒↪ : A ↠ B → B ↪ A -↠⇒↪ s = mk↪ {from = to} λ { ≡.refl → section-strictInverseˡ _ } +↠⇒↪ s = mk↪ {from = to} λ { ≡.refl → strictlyInverseˡ _ } where open Surjection s ↠⇒⇔ : A ↠ B → A ⇔ B @@ -80,7 +80,7 @@ module _ (surjection : Surjection S T) where injective⇒to⁻-cong : Injective Eq₁._≈_ Eq₂._≈_ to → Congruent Eq₂._≈_ Eq₁._≈_ section injective⇒to⁻-cong injective = - Symmetry.section-cong (injective , surjective) Eq₁.refl Eq₂.sym Eq₂.trans + Section.cong Eq₂._≈_ surjective injective Eq₁.refl Eq₂.sym Eq₂.trans {-# WARNING_ON_USAGE injective⇒to⁻-cong "Warning: injective⇒to⁻-cong was deprecated in v2.3. Please use Symmetry.section-cong instead. " From 3e15e992c53f360bfeeaa1acffe53ad7d5cbdf66 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 14:12:53 +0000 Subject: [PATCH 33/64] fix: use of rectified lemma names --- .../Product/Function/Dependent/Propositional.agda | 14 +++++++------- src/Data/Product/Function/Dependent/Setoid.agda | 8 ++++---- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/Data/Product/Function/Dependent/Propositional.agda b/src/Data/Product/Function/Dependent/Propositional.agda index e39ec31bdc..8bc6f71257 100644 --- a/src/Data/Product/Function/Dependent/Propositional.agda +++ b/src/Data/Product/Function/Dependent/Propositional.agda @@ -194,19 +194,19 @@ module _ where to′ = map (to I↠J) (to A↠B) backcast : ∀ {i} → B i → B (to I↠J (section I↠J i)) - backcast = ≡.subst B (≡.sym (section-strictInverseˡ I↠J _)) + backcast = ≡.subst B (≡.sym (strictlyInverseˡ I↠J _)) section′ : Σ J B → Σ I A section′ = map (section I↠J) (section A↠B ∘ backcast) strictlySurjective′ : StrictlySurjective _≡_ to′ strictlySurjective′ (x , y) = section′ (x , y) , Σ-≡,≡→≡ - ( section-strictInverseˡ I↠J x + ( strictlyInverseˡ I↠J x , (begin - ≡.subst B (section-strictInverseˡ I↠J x) (to A↠B (section A↠B (backcast y))) - ≡⟨ ≡.cong (≡.subst B _) (section-strictInverseˡ A↠B _) ⟩ - ≡.subst B (section-strictInverseˡ I↠J x) (backcast y) - ≡⟨ ≡.subst-subst-sym (section-strictInverseˡ I↠J x) ⟩ + ≡.subst B (strictlyInverseˡ I↠J x) (to A↠B (section A↠B (backcast y))) + ≡⟨ ≡.cong (≡.subst B _) (strictlyInverseˡ A↠B _) ⟩ + ≡.subst B (strictlyInverseˡ I↠J x) (backcast y) + ≡⟨ ≡.subst-subst-sym (strictlyInverseˡ I↠J x) ⟩ y ∎) ) where open ≡.≡-Reasoning @@ -254,7 +254,7 @@ module _ where Σ-↔ {I = I} {J = J} {A = A} {B = B} I↔J A↔B = mk↔ₛ′ (Surjection.to surjection′) (Surjection.section surjection′) - (Surjection.section-strictInverseˡ surjection′) + (Surjection.strictlyInverseˡ surjection′) left-inverse-of where open ≡.≡-Reasoning diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda index 32c52e5944..72fdd05347 100644 --- a/src/Data/Product/Function/Dependent/Setoid.agda +++ b/src/Data/Product/Function/Dependent/Setoid.agda @@ -122,8 +122,8 @@ module _ where B-from : ∀ {y} → Func (B atₛ y) (A atₛ (ItoJ.section y)) B-from = record - { to = from A⇔B ∘ cast B (ItoJ.section-strictInverseˡ _) - ; cong = from-cong A⇔B ∘ cast-cong B (ItoJ.section-strictInverseˡ _) + { to = from A⇔B ∘ cast B (ItoJ.strictlyInverseˡ _) + ; cong = from-cong A⇔B ∘ cast-cong B (ItoJ.strictlyInverseˡ _) } ------------------------------------------------------------------------ @@ -172,11 +172,11 @@ module _ where func = function (Surjection.function I↠J) (Surjection.function A↠B) section′ : Carrier (J ×ₛ B) → Carrier (I ×ₛ A) - section′ (j , y) = section I↠J j , section A↠B (cast B (section-strictInverseˡ I↠J _) y) + section′ (j , y) = section I↠J j , section A↠B (cast B (strictlyInverseˡ I↠J _) y) strictlySurj : StrictlySurjective (Func.Eq₂._≈_ func) (Func.to func) strictlySurj (j , y) = section′ (j , y) , - section-strictInverseˡ I↠J j , IndexedSetoid.trans B (section-strictInverseˡ A↠B _) (cast-eq B (section-strictInverseˡ I↠J j)) + strictlyInverseˡ I↠J j , IndexedSetoid.trans B (strictlyInverseˡ A↠B _) (cast-eq B (strictlyInverseˡ I↠J j)) surj : Surjective (Func.Eq₁._≈_ func) (Func.Eq₂._≈_ func) (Func.to func) surj = strictlySurjective⇒surjective (I ×ₛ A) (J ×ₛ B) (Func.cong func) strictlySurj From 679241e9ee9b978459e448c1adaf8e4e202e017b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 16:43:00 +0000 Subject: [PATCH 34/64] fix: deprecation warning --- src/Function/Properties/Surjection.agda | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda index d5dcf297fc..dfea90dd6d 100644 --- a/src/Function/Properties/Surjection.agda +++ b/src/Function/Properties/Surjection.agda @@ -11,9 +11,9 @@ module Function.Properties.Surjection where open import Function.Base using (_∘_; _$_) open import Function.Definitions using (Surjective; Injective; Congruent) open import Function.Bundles - using (Func; Surjection; _↠_; _⟶_; _↪_; mk↪; _⇔_; mk⇔) -open import Function.Consequences using (module Section) + using (Func; Surjection; Bijection; _↠_; _⟶_; _↪_; mk↪; _⇔_; mk⇔) import Function.Construct.Identity as Identity +import Function.Construct.Symmetry as Symmetry import Function.Construct.Composition as Compose open import Level using (Level) open import Data.Product.Base using (_,_; proj₁; proj₂) @@ -79,9 +79,13 @@ module _ (surjection : Surjection S T) where injective⇒to⁻-cong : Injective Eq₁._≈_ Eq₂._≈_ to → Congruent Eq₂._≈_ Eq₁._≈_ section - injective⇒to⁻-cong injective = - Section.cong Eq₂._≈_ surjective injective Eq₁.refl Eq₂.sym Eq₂.trans + injective⇒to⁻-cong injective = section-cong + where + SB : Bijection S T + SB = record { cong = cong ; bijective = injective , surjective } + open Bijection (Symmetry.bijectionWithoutCongruence SB) + using () renaming (cong to section-cong) {-# WARNING_ON_USAGE injective⇒to⁻-cong "Warning: injective⇒to⁻-cong was deprecated in v2.3. -Please use Symmetry.section-cong instead. " +Please use Function.Construct.Symmetry.bijectionWithoutCongruence instead. " #-} From ad7af967c932819224fcf51716e47946f3afaceb Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 17:29:28 +0000 Subject: [PATCH 35/64] fix: dependencies --- src/Function/Consequences.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda index 70f0a26f85..0aecb5b362 100644 --- a/src/Function/Consequences.agda +++ b/src/Function/Consequences.agda @@ -133,6 +133,9 @@ module Section (≈₂ : Rel B ℓ₂) (surj : Surjective {A = A} ≈₁ ≈₂ strictlyInverseˡ : StrictlyInverseˡ ≈₂ f section strictlyInverseˡ _ = inverseˡ refl + strictlyInverseʳ : StrictlyInverseʳ ≈₂ section f + strictlyInverseʳ _ = inverseˡ refl + injective : Symmetric ≈₂ → Transitive ≈₂ → Injective ≈₂ ≈₁ section injective sym trans = trans (sym (strictlyInverseˡ _)) ∘ inverseˡ @@ -146,9 +149,6 @@ module Section (≈₂ : Rel B ℓ₂) (surj : Surjective {A = A} ≈₁ ≈₂ inverseʳ : Transitive ≈₂ → Inverseʳ ≈₁ ≈₂ f section inverseʳ trans = inj ∘ trans (f∘section≡id _) - strictlyInverseʳ : Transitive ≈₂ → StrictlyInverseʳ ≈₂ section f - strictlyInverseʳ trans = inverseʳ⇒strictlyInverseʳ ≈₂ ≈₁ refl inverseˡ - surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ section surjective trans x = f x , inverseʳ trans From 6141208d6d7aba63e04e0297f9a15040085ea4a3 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 17:29:57 +0000 Subject: [PATCH 36/64] fix: dependencies --- src/Function/Structures.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index a70ef113e3..d999e24c6b 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -60,7 +60,7 @@ record IsInjection (to : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where open IsCongruent isCongruent public -record IsSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where +record IsSurjection (f : A → B ) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isCongruent : IsCongruent f surjective : Surjective _≈₁_ _≈₂_ f @@ -103,7 +103,7 @@ record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where inverseʳ = S.inverseʳ injective Eq₁.refl Eq₂.trans strictlyInverseʳ : StrictlyInverseʳ _≈₂_ section f - strictlyInverseʳ = S.strictlyInverseʳ injective Eq₁.refl Eq₂.trans + strictlyInverseʳ = S.strictlyInverseʳ Eq₁.refl ------------------------------------------------------------------------ From 9cbc30d49a865ed3c9188460bbcc4d4c0e05e3e0 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 17:30:29 +0000 Subject: [PATCH 37/64] add: `CHANGELOG` --- CHANGELOG.md | 87 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 87 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index f16ed00b65..4a7ce51e53 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,6 +6,11 @@ The library has been tested using Agda 2.7.0 and 2.7.0.1. Highlights ---------- +* A major overhaul of the `Function` hierarchy sees the systematic development + and use of theory of the left inverse to a given `Surjective` function `f`, in + `Function.Consequences.Section`, up to and including full symmetry of `Bijection`, in + `Function.Properties.Bijection`. + Bug-fixes --------- @@ -51,6 +56,32 @@ Deprecated names ∣∣-trans ↦ ∥-trans ``` +* In `Function.Bundles.IsSurjection`: + ```agda + to⁻ ↦ Function.Structures.IsSurjection.section + to∘to⁻ ↦ Function.Structures.IsSurjection.strictlyInverseˡ + ``` + +* In `Function.Construct.Symmetry`: + ```agda + injective ↦ Function.Consequences.Section.injective + surjective ↦ Function.Consequences.Section.surjective + bijective ↦ Function.Consequences.Section.bijective + isBijection ↦ isBijectionWithoutCongruence + isBijection-≡ ↦ isBijectionWithoutCongruence + bijection-≡ ↦ bijectionWithoutCongruence + ``` + +* In `Function.Properties.Bijection`: + ```agda + sym-≡ ↦ sym + ``` + +* In `Function.Properties.Surjection`: + ```agda + injective⇒to⁻-cong ↦ Function.Construct.Symmetry.bijectionWithoutCongruence + ``` + New modules ----------- @@ -85,3 +116,59 @@ Additions to existing modules quasiring : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ) commutativeRing : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ) ``` + +* In `Function.Bundles.Bijection`: + ```agda + section : B → A + inverseˡ : Inverseˡ _≈₁_ _≈₂_ to section + strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to section + inverseʳ : Inverseʳ _≈₁_ _≈₂_ to section + strictlyInverseʳ : StrictlyInverseʳ _≈₂_ section to + ``` + +* In `Function.Bundles.LeftInverse`: + ```agda + surjective : Surjective _≈₁_ _≈₂_ to + surjection : Surjection From To + ``` + +* In `Function.Bundles.RightInverse`: + ```agda + isInjection : IsInjection to + injective : Injective _≈₁_ _≈₂_ to + injection : Injection From To + ``` + +* In `Function.Bundles.Surjection`: + ```agda + section : B → A + inverseˡ : Inverseˡ _≈₁_ _≈₂_ to section + strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to section + ``` + +* In `Function.Consequences`: the theory of the left inverse of a surjective function + ```agda + module Section (surj : Surjective ≈₁ ≈₂ f) + ``` + +* In `Function.Properties.Bijection`: + ```agda + sym : Bijection S T → Bijection T S + ``` + +* In `Function.Structures.IsBijection`: + ```agda + section : B → A + inverseˡ : Inverseˡ _≈₁_ _≈₂_ f section + strictlyInverseˡ : StrictlyInverseˡ _≈₂_ f section + inverseʳ : Inverseʳ _≈₁_ _≈₂_ f section + strictlyInverseʳ : StrictlyInverseʳ _≈₂_ section f + ``` + +* In `Function.Structures.IsSurjection`: + ```agda + section : B → A + inverseˡ : Inverseˡ _≈₁_ _≈₂_ f section + strictlyInverseˡ : StrictlyInverseˡ _≈₂_ f section + ``` + From 325c66f2f10f7f5d48848c99fd73f33c7c7c0e7a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 30 Jan 2025 23:50:49 +0000 Subject: [PATCH 38/64] fix: version numbers in deprecations --- src/Function/Construct/Symmetry.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Function/Construct/Symmetry.agda b/src/Function/Construct/Symmetry.agda index b4b397ac78..fbd1e9c1ff 100644 --- a/src/Function/Construct/Symmetry.agda +++ b/src/Function/Construct/Symmetry.agda @@ -225,15 +225,15 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ S.section bijective sym trans _ = S.injective refl sym trans , surjective trans {-# WARNING_ON_USAGE injective -"Warning: injective was deprecated in v2.0. +"Warning: injective was deprecated in v2.3. Please use Function.Consequences.Section.injective instead, with a sharper type." #-} {-# WARNING_ON_USAGE surjective -"Warning: surjective was deprecated in v2.0. +"Warning: surjective was deprecated in v2.3. Please use Function.Consequences.Section.surjective instead." #-} {-# WARNING_ON_USAGE bijective -"Warning: bijective was deprecated in v2.0. +"Warning: bijective was deprecated in v2.3. Please use Function.Consequences.Section.bijective instead, with a sharper type." #-} From f981711cf8acf7a4ebd20e19d0d2056eda2ce542 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 31 Jan 2025 09:10:23 +0000 Subject: [PATCH 39/64] refactor: Luke, use the force! --- src/Function/Construct/Symmetry.agda | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/src/Function/Construct/Symmetry.agda b/src/Function/Construct/Symmetry.agda index fbd1e9c1ff..1414d1fdbd 100644 --- a/src/Function/Construct/Symmetry.agda +++ b/src/Function/Construct/Symmetry.agda @@ -22,7 +22,7 @@ open import Level using (Level) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive) open import Relation.Binary.Bundles using (Setoid) -open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong) +open import Relation.Binary.PropositionalEquality.Core using (_≡_) open import Relation.Binary.PropositionalEquality.Properties using (setoid) private @@ -47,8 +47,8 @@ module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) {f : A → B} {f⁻¹ : ------------------------------------------------------------------------ -- Structures -module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} - {f : A → B} (isBij : IsBijection ≈₁ ≈₂ f) +module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} + (isBij : IsBijection ≈₁ ≈₂ f) where private module B = IsBijection isBij @@ -105,11 +105,9 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} (bij : Bijection R S) where -- We can always flip a bijection WITHOUT knowing if the witness produced -- by the surjection proof respects the equality on the codomain. bijectionWithoutCongruence : Bijection S R - bijectionWithoutCongruence = record - { to = B.section - ; cong = S.cong B.injective B.Eq₁.refl B.Eq₂.sym B.Eq₂.trans - ; bijective = S.bijective B.injective B.Eq₁.refl B.Eq₂.sym B.Eq₂.trans - } where module B = Bijection bij ; module S = Section (Setoid._≈_ S) B.surjective + bijectionWithoutCongruence = record { + IsBijection (isBijectionWithoutCongruence B.isBijection) + } where module B = Bijection bij module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} where @@ -223,7 +221,7 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} bijective : Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ S.section - bijective sym trans _ = S.injective refl sym trans , surjective trans + bijective sym trans cong = injective sym trans cong , surjective trans {-# WARNING_ON_USAGE injective "Warning: injective was deprecated in v2.3. Please use Function.Consequences.Section.injective instead, with a sharper type." @@ -237,8 +235,8 @@ Please use Function.Consequences.Section.surjective instead." Please use Function.Consequences.Section.bijective instead, with a sharper type." #-} -module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} - {f : A → B} (isBij : IsBijection ≈₁ ≈₂ f) +module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} + (isBij : IsBijection ≈₁ ≈₂ f) where private module B = IsBijection isBij isBijection : Congruent ≈₂ ≈₁ B.section → IsBijection ≈₂ ≈₁ B.section From 629f00ce443477dae712e5889c17467d2b582caf Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 31 Jan 2025 10:16:58 +0000 Subject: [PATCH 40/64] fix: streamlining --- src/Function/Consequences.agda | 20 +++++++++----------- src/Function/Structures.agda | 10 +++++----- 2 files changed, 14 insertions(+), 16 deletions(-) diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda index 0aecb5b362..7cff76831b 100644 --- a/src/Function/Consequences.agda +++ b/src/Function/Consequences.agda @@ -50,8 +50,7 @@ inverseʳ⇒injective : ∀ (≈₂ : Rel B ℓ₂) f → Transitive ≈₁ → Inverseʳ ≈₁ ≈₂ f f⁻¹ → Injective ≈₁ ≈₂ f -inverseʳ⇒injective ≈₂ f refl sym trans invʳ {x} {y} fx≈fy = - trans (sym (invʳ refl)) (invʳ fx≈fy) +inverseʳ⇒injective ≈₂ f refl sym trans invʳ = trans (sym (invʳ refl)) ∘ invʳ ------------------------------------------------------------------------ -- Inverseᵇ @@ -69,16 +68,15 @@ inverseᵇ⇒bijective {f = f} ≈₂ refl sym trans (invˡ , invʳ) = -- StrictlySurjective surjective⇒strictlySurjective : ∀ (≈₂ : Rel B ℓ₂) → - Reflexive ≈₁ → - Surjective ≈₁ ≈₂ f → - StrictlySurjective ≈₂ f -surjective⇒strictlySurjective _ refl surj x = - Product.map₂ (λ v → v refl) (surj x) + Reflexive ≈₁ → + Surjective ≈₁ ≈₂ f → + StrictlySurjective ≈₂ f +surjective⇒strictlySurjective _ refl surj = Product.map₂ (λ v → v refl) ∘ surj strictlySurjective⇒surjective : Transitive ≈₂ → - Congruent ≈₁ ≈₂ f → - StrictlySurjective ≈₂ f → - Surjective ≈₁ ≈₂ f + Congruent ≈₁ ≈₂ f → + StrictlySurjective ≈₂ f → + Surjective ≈₁ ≈₂ f strictlySurjective⇒surjective trans cong surj x = Product.map₂ (λ fy≈x z≈y → trans (cong z≈y) fy≈x) (surj x) @@ -134,7 +132,7 @@ module Section (≈₂ : Rel B ℓ₂) (surj : Surjective {A = A} ≈₁ ≈₂ strictlyInverseˡ _ = inverseˡ refl strictlyInverseʳ : StrictlyInverseʳ ≈₂ section f - strictlyInverseʳ _ = inverseˡ refl + strictlyInverseʳ = strictlyInverseˡ injective : Symmetric ≈₂ → Transitive ≈₂ → Injective ≈₂ ≈₁ section injective sym trans = trans (sym (strictlyInverseˡ _)) ∘ inverseˡ diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index d999e24c6b..7f199a50bd 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -60,7 +60,7 @@ record IsInjection (to : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where open IsCongruent isCongruent public -record IsSurjection (f : A → B ) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where +record IsSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isCongruent : IsCongruent f surjective : Surjective _≈₁_ _≈₂_ f @@ -75,7 +75,7 @@ record IsSurjection (f : A → B ) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where strictlySurjective = S.strictlySurjective Eq₁.refl strictlyInverseˡ : StrictlyInverseˡ _≈₂_ f section - strictlyInverseˡ _ = S.inverseˡ Eq₁.refl + strictlyInverseˡ _ = inverseˡ Eq₁.refl record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where @@ -120,7 +120,7 @@ record IsLeftInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ renaming (cong to to-cong) strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from - strictlyInverseˡ = inverseˡ⇒strictlyInverseˡ _≈₁_ _≈₂_ Eq₁.refl inverseˡ + strictlyInverseˡ _ = inverseˡ Eq₁.refl isSurjection : IsSurjection to isSurjection = record @@ -139,10 +139,10 @@ record IsRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ renaming (cong to to-cong) strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from - strictlyInverseʳ = inverseʳ⇒strictlyInverseʳ _≈₁_ _≈₂_ Eq₂.refl inverseʳ + strictlyInverseʳ _ = inverseʳ Eq₂.refl injective : Injective _≈₁_ _≈₂_ to - injective = inverseʳ⇒injective {f⁻¹ = from} _≈₂_ to Eq₂.refl Eq₁.sym Eq₁.trans inverseʳ + injective = inverseʳ⇒injective _≈₂_ to Eq₂.refl Eq₁.sym Eq₁.trans inverseʳ isInjection : IsInjection to isInjection = record From 79afa5b706c9087c7af95555c61b9878bed7eb10 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 31 Jan 2025 10:17:36 +0000 Subject: [PATCH 41/64] fix: streamlining --- src/Function/Structures.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index 7f199a50bd..8e4073b8da 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -17,7 +17,7 @@ module Function.Structures {a b ℓ₁ ℓ₂} {B : Set b} (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain where -open import Data.Product.Base as Product using (∃; _×_; _,_; proj₁; proj₂) +open import Data.Product.Base as Product using (∃; _×_; _,_) open import Function.Base open import Function.Consequences open import Function.Definitions From d8ec317a76e49f3317b698fd32b93658527e9e9b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 31 Jan 2025 10:52:21 +0000 Subject: [PATCH 42/64] =?UTF-8?q?fix:=20type,=20and=20definition,=20of=20`?= =?UTF-8?q?strictlyInverse=CA=B3`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CHANGELOG.md | 4 ++-- src/Function/Consequences.agda | 6 +++--- src/Function/Structures.agda | 4 ++-- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4a7ce51e53..c1a37cff67 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -123,7 +123,7 @@ Additions to existing modules inverseˡ : Inverseˡ _≈₁_ _≈₂_ to section strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to section inverseʳ : Inverseʳ _≈₁_ _≈₂_ to section - strictlyInverseʳ : StrictlyInverseʳ _≈₂_ section to + strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to section ``` * In `Function.Bundles.LeftInverse`: @@ -162,7 +162,7 @@ Additions to existing modules inverseˡ : Inverseˡ _≈₁_ _≈₂_ f section strictlyInverseˡ : StrictlyInverseˡ _≈₂_ f section inverseʳ : Inverseʳ _≈₁_ _≈₂_ f section - strictlyInverseʳ : StrictlyInverseʳ _≈₂_ section f + strictlyInverseʳ : StrictlyInverseʳ _≈₁_ f section ``` * In `Function.Structures.IsSurjection`: diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda index 7cff76831b..3748474788 100644 --- a/src/Function/Consequences.agda +++ b/src/Function/Consequences.agda @@ -131,9 +131,6 @@ module Section (≈₂ : Rel B ℓ₂) (surj : Surjective {A = A} ≈₁ ≈₂ strictlyInverseˡ : StrictlyInverseˡ ≈₂ f section strictlyInverseˡ _ = inverseˡ refl - strictlyInverseʳ : StrictlyInverseʳ ≈₂ section f - strictlyInverseʳ = strictlyInverseˡ - injective : Symmetric ≈₂ → Transitive ≈₂ → Injective ≈₂ ≈₁ section injective sym trans = trans (sym (strictlyInverseˡ _)) ∘ inverseˡ @@ -147,6 +144,9 @@ module Section (≈₂ : Rel B ℓ₂) (surj : Surjective {A = A} ≈₁ ≈₂ inverseʳ : Transitive ≈₂ → Inverseʳ ≈₁ ≈₂ f section inverseʳ trans = inj ∘ trans (f∘section≡id _) + strictlyInverseʳ : Reflexive ≈₂ → Transitive ≈₂ → StrictlyInverseʳ ≈₁ f section + strictlyInverseʳ refl trans _ = inverseʳ trans refl + surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ section surjective trans x = f x , inverseʳ trans diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index 8e4073b8da..6eadbfd3cf 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -102,8 +102,8 @@ record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where inverseʳ : Inverseʳ _≈₁_ _≈₂_ f section inverseʳ = S.inverseʳ injective Eq₁.refl Eq₂.trans - strictlyInverseʳ : StrictlyInverseʳ _≈₂_ section f - strictlyInverseʳ = S.strictlyInverseʳ Eq₁.refl + strictlyInverseʳ : StrictlyInverseʳ _≈₁_ f section + strictlyInverseʳ _ = inverseʳ Eq₂.refl ------------------------------------------------------------------------ From 2326602d4403c1ee454e885286d8aaa6079a930c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 1 Feb 2025 09:24:08 +0000 Subject: [PATCH 43/64] tweak; `import` list --- src/Function/Bundles.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index 926b636c93..c8a34c85f5 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -20,6 +20,7 @@ module Function.Bundles where open import Function.Base using (_∘_) +open import Function.Consequences.Propositional open import Function.Definitions import Function.Structures as FunctionStructures open import Level using (Level; _⊔_; suc) @@ -28,7 +29,6 @@ open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) import Relation.Binary.PropositionalEquality.Properties as ≡ -open import Function.Consequences.Propositional open Setoid using (isEquivalence) private From 1156681f5eeda171417a6bc439488d0c76e91484 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 1 Feb 2025 12:59:43 +0000 Subject: [PATCH 44/64] refactor: add `Setoid` version of module `Section` --- src/Function/Consequences/Setoid.agda | 35 +++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/src/Function/Consequences/Setoid.agda b/src/Function/Consequences/Setoid.agda index d2c3b948d9..64cc407d7f 100644 --- a/src/Function/Consequences/Setoid.agda +++ b/src/Function/Consequences/Setoid.agda @@ -90,3 +90,38 @@ strictlyInverseʳ⇒inverseʳ : Congruent ≈₂ ≈₁ f⁻¹ → StrictlyInverseʳ ≈₁ f f⁻¹ → Inverseʳ ≈₁ ≈₂ f f⁻¹ strictlyInverseʳ⇒inverseʳ = C.strictlyInverseʳ⇒inverseʳ S.trans + +------------------------------------------------------------------------ +-- Section + +module Section (surj : Surjective ≈₁ ≈₂ f) where + + private module Sf = C.Section ≈₂ surj + + open Sf public using (section; inverseˡ) + + strictlySurjective : StrictlySurjective ≈₂ f + strictlySurjective = Sf.strictlySurjective S.refl + + strictlyInverseˡ : StrictlyInverseˡ ≈₂ f section + strictlyInverseˡ = Sf.strictlyInverseˡ S.refl + + injective : Injective ≈₂ ≈₁ section + injective = Sf.injective S.refl T.sym T.trans + + module _ (inj : Injective ≈₁ ≈₂ f) where + + cong : Congruent ≈₂ ≈₁ section + cong = Sf.cong inj S.refl T.sym T.trans + + inverseʳ : Inverseʳ ≈₁ ≈₂ f section + inverseʳ = Sf.inverseʳ inj S.refl T.trans + + strictlyInverseʳ : StrictlyInverseʳ ≈₁ f section + strictlyInverseʳ = Sf.strictlyInverseʳ inj S.refl T.refl T.trans + + surjective : Surjective ≈₂ ≈₁ section + surjective = Sf.surjective inj S.refl T.trans + + bijective : Bijective ≈₂ ≈₁ section + bijective = Sf.bijective inj S.refl T.sym T.trans From 9115dd765e293116f5d7e02d168abc28452b3d0b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 1 Feb 2025 13:09:30 +0000 Subject: [PATCH 45/64] refactor: propagate definitions --- src/Function/Structures.agda | 27 ++++++++++----------------- 1 file changed, 10 insertions(+), 17 deletions(-) diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index 6eadbfd3cf..8f3776fd19 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -19,7 +19,7 @@ module Function.Structures {a b ℓ₁ ℓ₂} open import Data.Product.Base as Product using (∃; _×_; _,_) open import Function.Base -open import Function.Consequences +open import Function.Consequences.Setoid open import Function.Definitions open import Level using (_⊔_) @@ -67,15 +67,8 @@ record IsSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where open IsCongruent isCongruent public - private module S = Section _≈₂_ surjective - - open S public using (section; inverseˡ) - - strictlySurjective : StrictlySurjective _≈₂_ f - strictlySurjective = S.strictlySurjective Eq₁.refl - - strictlyInverseˡ : StrictlyInverseˡ _≈₂_ f section - strictlyInverseˡ _ = inverseˡ Eq₁.refl + open Section Eq₁.setoid Eq₂.setoid surjective public + using (section; inverseˡ; strictlyInverseˡ; strictlySurjective) record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where @@ -94,16 +87,16 @@ record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where ; surjective = surjective } - open IsSurjection isSurjection public - using (strictlySurjective; section; inverseˡ; strictlyInverseˡ) + private module S = Section Eq₁.setoid Eq₂.setoid surjective - private module S = Section _≈₂_ surjective + open S public + using (strictlySurjective; section; inverseˡ; strictlyInverseˡ) inverseʳ : Inverseʳ _≈₁_ _≈₂_ f section - inverseʳ = S.inverseʳ injective Eq₁.refl Eq₂.trans + inverseʳ = S.inverseʳ injective strictlyInverseʳ : StrictlyInverseʳ _≈₁_ f section - strictlyInverseʳ _ = inverseʳ Eq₂.refl + strictlyInverseʳ = S.strictlyInverseʳ injective ------------------------------------------------------------------------ @@ -125,7 +118,7 @@ record IsLeftInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ isSurjection : IsSurjection to isSurjection = record { isCongruent = isCongruent - ; surjective = inverseˡ⇒surjective _≈₂_ inverseˡ + ; surjective = inverseˡ⇒surjective Eq₁.setoid Eq₂.setoid inverseˡ } @@ -142,7 +135,7 @@ record IsRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ strictlyInverseʳ _ = inverseʳ Eq₂.refl injective : Injective _≈₁_ _≈₂_ to - injective = inverseʳ⇒injective _≈₂_ to Eq₂.refl Eq₁.sym Eq₁.trans inverseʳ + injective = inverseʳ⇒injective Eq₁.setoid Eq₂.setoid to inverseʳ isInjection : IsInjection to isInjection = record From 3c577cf910eca4122dc6f59d718028ea21ddc577 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 1 Feb 2025 13:14:48 +0000 Subject: [PATCH 46/64] fix: update `CHANGELOG` --- CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index c1a37cff67..757919f4e8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -146,7 +146,8 @@ Additions to existing modules strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to section ``` -* In `Function.Consequences`: the theory of the left inverse of a surjective function +* In `Function.Consequences` and `Function.Consequences.Setoid`: + the theory of the left inverse of a surjective function ```agda module Section (surj : Surjective ≈₁ ≈₂ f) ``` From 8d072d64a030cea7582868e8a115d406ad841725 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 2 Feb 2025 14:46:12 +0000 Subject: [PATCH 47/64] fix: add missing entries! --- CHANGELOG.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 757919f4e8..daff8029e0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -152,6 +152,12 @@ Additions to existing modules module Section (surj : Surjective ≈₁ ≈₂ f) ``` +* In `Function.Construct.Symmetry`: + ```agda + isBijectionWithoutCongruence : (IsBijection ≈₁ ≈₂ f) → IsBijection ≈₂ ≈₁ section + bijectionWithoutCongruence : (Bijection R S) → IsBijection S R + ``` + * In `Function.Properties.Bijection`: ```agda sym : Bijection S T → Bijection T S From 7bd938c5fbae5f68a7d6996b53e84defc714acaf Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 2 Feb 2025 15:01:01 +0000 Subject: [PATCH 48/64] refactor: exploit duality; cherry-picked from #2567 --- src/Function/Consequences.agda | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda index 3748474788..d0d4b09c4f 100644 --- a/src/Function/Consequences.agda +++ b/src/Function/Consequences.agda @@ -31,7 +31,7 @@ private contraInjective : ∀ (≈₂ : Rel B ℓ₂) → Injective ≈₁ ≈₂ f → ∀ {x y} → ¬ (≈₁ x y) → ¬ (≈₂ (f x) (f y)) -contraInjective _ inj p = contraposition inj p +contraInjective _ inj = contraposition inj ------------------------------------------------------------------------ -- Inverseˡ @@ -39,7 +39,7 @@ contraInjective _ inj p = contraposition inj p inverseˡ⇒surjective : ∀ (≈₂ : Rel B ℓ₂) → Inverseˡ ≈₁ ≈₂ f f⁻¹ → Surjective ≈₁ ≈₂ f -inverseˡ⇒surjective ≈₂ invˡ y = (_ , invˡ) +inverseˡ⇒surjective ≈₂ invˡ _ = (_ , invˡ) ------------------------------------------------------------------------ -- Inverseʳ @@ -103,14 +103,15 @@ inverseʳ⇒strictlyInverseʳ : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ Reflexive ≈₂ → Inverseʳ ≈₁ ≈₂ f f⁻¹ → StrictlyInverseʳ ≈₁ f f⁻¹ -inverseʳ⇒strictlyInverseʳ _ _ refl sinv x = sinv refl +inverseʳ⇒strictlyInverseʳ {f = f} {f⁻¹ = f⁻¹} ≈₁ ≈₂ = + inverseˡ⇒strictlyInverseˡ {f = f⁻¹} {f⁻¹ = f} ≈₂ ≈₁ strictlyInverseʳ⇒inverseʳ : Transitive ≈₁ → Congruent ≈₂ ≈₁ f⁻¹ → StrictlyInverseʳ ≈₁ f f⁻¹ → Inverseʳ ≈₁ ≈₂ f f⁻¹ -strictlyInverseʳ⇒inverseʳ trans cong sinv {x} y≈f⁻¹x = - trans (cong y≈f⁻¹x) (sinv x) +strictlyInverseʳ⇒inverseʳ {≈₁ = ≈₁} {≈₂ = ≈₂} {f⁻¹ = f⁻¹} {f = f} = + strictlyInverseˡ⇒inverseˡ {≈₂ = ≈₁} {≈₁ = ≈₂} {f = f⁻¹} {f⁻¹ = f} ------------------------------------------------------------------------ -- Theory of the section of a Surjective function From 0997c712c00f561d2dcd4936fbf38007569ba653 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 2 Feb 2025 15:36:02 +0000 Subject: [PATCH 49/64] fix: typo --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index daff8029e0..1569a568f0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -155,7 +155,7 @@ Additions to existing modules * In `Function.Construct.Symmetry`: ```agda isBijectionWithoutCongruence : (IsBijection ≈₁ ≈₂ f) → IsBijection ≈₂ ≈₁ section - bijectionWithoutCongruence : (Bijection R S) → IsBijection S R + bijectionWithoutCongruence : (Bijection R S) → Bijection S R ``` * In `Function.Properties.Bijection`: From 86dab2d1c9c012365822ba96e5727acba076627d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 2 Feb 2025 17:24:52 +0000 Subject: [PATCH 50/64] fix: add more fields/missing `CHANGELOG` entries! --- CHANGELOG.md | 11 +++++++++++ src/Function/Structures.agda | 4 +++- 2 files changed, 14 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1569a568f0..f43644c324 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -172,6 +172,17 @@ Additions to existing modules strictlyInverseʳ : StrictlyInverseʳ _≈₁_ f section ``` +* In `Function.Structures.IsLeftInverse`: + ```agda + surjective : Surjective _≈₁_ _≈₂_ to + ``` + +* In `Function.Structures.IsRightInverse`: + ```agda + injective : Injective _≈₁_ _≈₂_ to + isInjection : IsInjection to + ``` + * In `Function.Structures.IsSurjection`: ```agda section : B → A diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index 8f3776fd19..175bc1ac34 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -115,10 +115,12 @@ record IsLeftInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from strictlyInverseˡ _ = inverseˡ Eq₁.refl + surjective = inverseˡ⇒surjective Eq₁.setoid Eq₂.setoid inverseˡ + isSurjection : IsSurjection to isSurjection = record { isCongruent = isCongruent - ; surjective = inverseˡ⇒surjective Eq₁.setoid Eq₂.setoid inverseˡ + ; surjective = surjective } From 90b30f11b52ed1401e4c99e2c810d95ccc7aca38 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 5 Feb 2025 07:55:19 +0000 Subject: [PATCH 51/64] refactor: rename `section` to `from`, plus some additional `to` infrastructure --- .../Function/Dependent/Propositional.agda | 12 +++---- .../Product/Function/Dependent/Setoid.agda | 4 +-- src/Function/Bundles.agda | 10 +++--- src/Function/Consequences.agda | 36 +++++++++---------- src/Function/Consequences/Setoid.agda | 24 ++++++------- src/Function/Construct/Symmetry.agda | 12 +++---- src/Function/Properties/Surjection.agda | 8 ++--- src/Function/Structures.agda | 24 ++++++------- 8 files changed, 65 insertions(+), 65 deletions(-) diff --git a/src/Data/Product/Function/Dependent/Propositional.agda b/src/Data/Product/Function/Dependent/Propositional.agda index 8bc6f71257..7008117ede 100644 --- a/src/Data/Product/Function/Dependent/Propositional.agda +++ b/src/Data/Product/Function/Dependent/Propositional.agda @@ -57,7 +57,7 @@ module _ where Σ I A ⇔ Σ J B Σ-⇔ {B = B} I↠J A⇔B = mk⇔ (map (to I↠J) (Equivalence.to A⇔B)) - (map (section I↠J) (Equivalence.from A⇔B ∘ ≡.subst B (≡.sym (proj₂ (surjective I↠J _) ≡.refl)))) + (map (from I↠J) (Equivalence.from A⇔B ∘ ≡.subst B (≡.sym (proj₂ (surjective I↠J _) ≡.refl)))) -- See also Data.Product.Relation.Binary.Pointwise.Dependent.WithK.↣. @@ -193,17 +193,17 @@ module _ where to′ : Σ I A → Σ J B to′ = map (to I↠J) (to A↠B) - backcast : ∀ {i} → B i → B (to I↠J (section I↠J i)) + backcast : ∀ {i} → B i → B (to I↠J (from I↠J i)) backcast = ≡.subst B (≡.sym (strictlyInverseˡ I↠J _)) section′ : Σ J B → Σ I A - section′ = map (section I↠J) (section A↠B ∘ backcast) + section′ = map (from I↠J) (from A↠B ∘ backcast) strictlySurjective′ : StrictlySurjective _≡_ to′ strictlySurjective′ (x , y) = section′ (x , y) , Σ-≡,≡→≡ ( strictlyInverseˡ I↠J x , (begin - ≡.subst B (strictlyInverseˡ I↠J x) (to A↠B (section A↠B (backcast y))) + ≡.subst B (strictlyInverseˡ I↠J x) (to A↠B (from A↠B (backcast y))) ≡⟨ ≡.cong (≡.subst B _) (strictlyInverseˡ A↠B _) ⟩ ≡.subst B (strictlyInverseˡ I↠J x) (backcast y) ≡⟨ ≡.subst-subst-sym (strictlyInverseˡ I↠J x) ⟩ @@ -253,7 +253,7 @@ module _ where Σ I A ↔ Σ J B Σ-↔ {I = I} {J = J} {A = A} {B = B} I↔J A↔B = mk↔ₛ′ (Surjection.to surjection′) - (Surjection.section surjection′) + (Surjection.from surjection′) (Surjection.strictlyInverseˡ surjection′) left-inverse-of where @@ -264,7 +264,7 @@ module _ where surjection′ : Σ I A ↠ Σ J B surjection′ = Σ-↠ (↔⇒↠ (≃⇒↔ I≃J)) (↔⇒↠ A↔B) - left-inverse-of : ∀ p → Surjection.section surjection′ (Surjection.to surjection′ p) ≡ p + left-inverse-of : ∀ p → Surjection.from surjection′ (Surjection.to surjection′ p) ≡ p left-inverse-of (x , y) = to Σ-≡,≡↔≡ ( _≃_.left-inverse-of I≃J x , (≡.subst A (_≃_.left-inverse-of I≃J x) diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda index 72fdd05347..2303230da5 100644 --- a/src/Data/Product/Function/Dependent/Setoid.agda +++ b/src/Data/Product/Function/Dependent/Setoid.agda @@ -120,7 +120,7 @@ module _ where B-to : ∀ {x} → Func (A atₛ x) (B atₛ (ItoJ.to x)) B-to = toFunction A⇔B - B-from : ∀ {y} → Func (B atₛ y) (A atₛ (ItoJ.section y)) + B-from : ∀ {y} → Func (B atₛ y) (A atₛ (ItoJ.from y)) B-from = record { to = from A⇔B ∘ cast B (ItoJ.strictlyInverseˡ _) ; cong = from-cong A⇔B ∘ cast-cong B (ItoJ.strictlyInverseˡ _) @@ -172,7 +172,7 @@ module _ where func = function (Surjection.function I↠J) (Surjection.function A↠B) section′ : Carrier (J ×ₛ B) → Carrier (I ×ₛ A) - section′ (j , y) = section I↠J j , section A↠B (cast B (strictlyInverseˡ I↠J _) y) + section′ (j , y) = from I↠J j , from A↠B (cast B (strictlyInverseˡ I↠J _) y) strictlySurj : StrictlySurjective (Func.Eq₂._≈_ func) (Func.to func) strictlySurj (j , y) = section′ (j , y) , diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index c8a34c85f5..544240671a 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -112,19 +112,19 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where open IsSurjection isSurjection public using ( strictlySurjective - ; section + ; from ; inverseˡ ; strictlyInverseˡ ) to⁻ : B → A - to⁻ = section + to⁻ = from {-# WARNING_ON_USAGE to⁻ "Warning: to⁻ was deprecated in v2.3. - Please use Function.Structures.IsSurjection.section instead. " + Please use Function.Structures.IsSurjection.from instead. " #-} - to∘to⁻ : StrictlyInverseˡ _≈₂_ to section + to∘to⁻ : StrictlyInverseˡ _≈₂_ to from to∘to⁻ = strictlyInverseˡ {-# WARNING_ON_USAGE to∘to⁻ "Warning: to∘to⁻ was deprecated in v2.3. @@ -161,7 +161,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where open Surjection surjection public using (isSurjection ; strictlySurjective - ; section + ; from ; inverseˡ ; strictlyInverseˡ ) diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda index d0d4b09c4f..8e77e8b03d 100644 --- a/src/Function/Consequences.agda +++ b/src/Function/Consequences.agda @@ -24,7 +24,7 @@ private a b ℓ₁ ℓ₂ : Level A B : Set a ≈₁ ≈₂ : Rel A ℓ₁ - f f⁻¹ : A → B + to f f⁻¹ : A → B ------------------------------------------------------------------------ -- Injective @@ -116,40 +116,40 @@ strictlyInverseʳ⇒inverseʳ {≈₁ = ≈₁} {≈₂ = ≈₂} {f⁻¹ = f⁻ ------------------------------------------------------------------------ -- Theory of the section of a Surjective function -module Section (≈₂ : Rel B ℓ₂) (surj : Surjective {A = A} ≈₁ ≈₂ f) where +module Section (≈₂ : Rel B ℓ₂) (surj : Surjective {A = A} ≈₁ ≈₂ to) where - section : B → A - section = proj₁ ∘ surj + from : B → A + from = proj₁ ∘ surj - inverseˡ : Inverseˡ ≈₁ ≈₂ f section + inverseˡ : Inverseˡ ≈₁ ≈₂ to from inverseˡ {x = x} = proj₂ (surj x) module _ (refl : Reflexive ≈₁) where - strictlySurjective : StrictlySurjective ≈₂ f + strictlySurjective : StrictlySurjective ≈₂ to strictlySurjective = surjective⇒strictlySurjective ≈₂ refl surj - strictlyInverseˡ : StrictlyInverseˡ ≈₂ f section + strictlyInverseˡ : StrictlyInverseˡ ≈₂ to from strictlyInverseˡ _ = inverseˡ refl - injective : Symmetric ≈₂ → Transitive ≈₂ → Injective ≈₂ ≈₁ section + injective : Symmetric ≈₂ → Transitive ≈₂ → Injective ≈₂ ≈₁ from injective sym trans = trans (sym (strictlyInverseˡ _)) ∘ inverseˡ - module _ (inj : Injective ≈₁ ≈₂ f) (refl : Reflexive ≈₁) where + module _ (inj : Injective ≈₁ ≈₂ to) (refl : Reflexive ≈₁) where - private f∘section≡id = strictlyInverseˡ refl + private to∘from≡id = strictlyInverseˡ refl - cong : Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₂ ≈₁ section - cong sym trans = inj ∘ trans (f∘section≡id _) ∘ sym ∘ trans (f∘section≡id _) ∘ sym + cong : Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₂ ≈₁ from + cong sym trans = inj ∘ trans (to∘from≡id _) ∘ sym ∘ trans (to∘from≡id _) ∘ sym - inverseʳ : Transitive ≈₂ → Inverseʳ ≈₁ ≈₂ f section - inverseʳ trans = inj ∘ trans (f∘section≡id _) + inverseʳ : Transitive ≈₂ → Inverseʳ ≈₁ ≈₂ to from + inverseʳ trans = inj ∘ trans (to∘from≡id _) - strictlyInverseʳ : Reflexive ≈₂ → Transitive ≈₂ → StrictlyInverseʳ ≈₁ f section + strictlyInverseʳ : Reflexive ≈₂ → Transitive ≈₂ → StrictlyInverseʳ ≈₁ to from strictlyInverseʳ refl trans _ = inverseʳ trans refl - surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ section - surjective trans x = f x , inverseʳ trans + surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ from + surjective trans x = to x , inverseʳ trans - bijective : Symmetric ≈₂ → Transitive ≈₂ → Bijective ≈₂ ≈₁ section + bijective : Symmetric ≈₂ → Transitive ≈₂ → Bijective ≈₂ ≈₁ from bijective sym trans = injective refl sym trans , surjective trans diff --git a/src/Function/Consequences/Setoid.agda b/src/Function/Consequences/Setoid.agda index 64cc407d7f..98669b0606 100644 --- a/src/Function/Consequences/Setoid.agda +++ b/src/Function/Consequences/Setoid.agda @@ -25,7 +25,7 @@ private open module T = Setoid T using () renaming (Carrier to B; _≈_ to ≈₂) variable - f : A → B + to f : A → B f⁻¹ : B → A ------------------------------------------------------------------------ @@ -94,34 +94,34 @@ strictlyInverseʳ⇒inverseʳ = C.strictlyInverseʳ⇒inverseʳ S.trans ------------------------------------------------------------------------ -- Section -module Section (surj : Surjective ≈₁ ≈₂ f) where +module Section (surj : Surjective ≈₁ ≈₂ to) where private module Sf = C.Section ≈₂ surj - open Sf public using (section; inverseˡ) + open Sf public using (from; inverseˡ) - strictlySurjective : StrictlySurjective ≈₂ f + strictlySurjective : StrictlySurjective ≈₂ to strictlySurjective = Sf.strictlySurjective S.refl - strictlyInverseˡ : StrictlyInverseˡ ≈₂ f section + strictlyInverseˡ : StrictlyInverseˡ ≈₂ to from strictlyInverseˡ = Sf.strictlyInverseˡ S.refl - injective : Injective ≈₂ ≈₁ section + injective : Injective ≈₂ ≈₁ from injective = Sf.injective S.refl T.sym T.trans - module _ (inj : Injective ≈₁ ≈₂ f) where + module _ (inj : Injective ≈₁ ≈₂ to) where - cong : Congruent ≈₂ ≈₁ section + cong : Congruent ≈₂ ≈₁ from cong = Sf.cong inj S.refl T.sym T.trans - inverseʳ : Inverseʳ ≈₁ ≈₂ f section + inverseʳ : Inverseʳ ≈₁ ≈₂ to from inverseʳ = Sf.inverseʳ inj S.refl T.trans - strictlyInverseʳ : StrictlyInverseʳ ≈₁ f section + strictlyInverseʳ : StrictlyInverseʳ ≈₁ to from strictlyInverseʳ = Sf.strictlyInverseʳ inj S.refl T.refl T.trans - surjective : Surjective ≈₂ ≈₁ section + surjective : Surjective ≈₂ ≈₁ from surjective = Sf.surjective inj S.refl T.trans - bijective : Bijective ≈₂ ≈₁ section + bijective : Bijective ≈₂ ≈₁ from bijective = Sf.bijective inj S.refl T.sym T.trans diff --git a/src/Function/Construct/Symmetry.agda b/src/Function/Construct/Symmetry.agda index 1414d1fdbd..6a7ec8543e 100644 --- a/src/Function/Construct/Symmetry.agda +++ b/src/Function/Construct/Symmetry.agda @@ -55,7 +55,7 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} -- We can ALWAYS flip a bijection, WITHOUT knowing the witness produced -- by the surjection proof respects the equality on the codomain. - isBijectionWithoutCongruence : IsBijection ≈₂ ≈₁ B.section + isBijectionWithoutCongruence : IsBijection ≈₂ ≈₁ B.from isBijectionWithoutCongruence = record { isInjection = record { isCongruent = record @@ -213,14 +213,14 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} module S = Section ≈₂ surj injective : Symmetric ≈₂ → Transitive ≈₂ → - Congruent ≈₁ ≈₂ f → Injective ≈₂ ≈₁ S.section + Congruent ≈₁ ≈₂ f → Injective ≈₂ ≈₁ S.from injective sym trans _ = S.injective refl sym trans - surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ S.section + surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ S.from surjective = S.surjective inj refl bijective : Symmetric ≈₂ → Transitive ≈₂ → - Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ S.section + Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ S.from bijective sym trans cong = injective sym trans cong , surjective trans {-# WARNING_ON_USAGE injective "Warning: injective was deprecated in v2.3. @@ -239,7 +239,7 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} (isBij : IsBijection ≈₁ ≈₂ f) where private module B = IsBijection isBij - isBijection : Congruent ≈₂ ≈₁ B.section → IsBijection ≈₂ ≈₁ B.section + isBijection : Congruent ≈₂ ≈₁ B.from → IsBijection ≈₂ ≈₁ B.from isBijection _ = isBijectionWithoutCongruence isBij {-# WARNING_ON_USAGE isBijection "Warning: isBijection was deprecated in v2.3. @@ -256,7 +256,7 @@ Please use isBijectionWithoutCongruence instead, with a sharper type." module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} (bij : Bijection R S) where private module B = Bijection bij - bijection : Congruent B.Eq₂._≈_ B.Eq₁._≈_ B.section → Bijection S R + bijection : Congruent B.Eq₂._≈_ B.Eq₁._≈_ B.from → Bijection S R bijection _ = bijectionWithoutCongruence bij bijection-≡ : {R : Setoid a ℓ₁} {B : Set b} → diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda index dfea90dd6d..1a22e0a81f 100644 --- a/src/Function/Properties/Surjection.agda +++ b/src/Function/Properties/Surjection.agda @@ -50,7 +50,7 @@ mkSurjection f surjective = record where open Surjection s ↠⇒⇔ : A ↠ B → A ⇔ B -↠⇒⇔ s = mk⇔ to section +↠⇒⇔ s = mk⇔ to from where open Surjection s ------------------------------------------------------------------------ @@ -78,13 +78,13 @@ module _ (surjection : Surjection S T) where open Surjection surjection injective⇒to⁻-cong : Injective Eq₁._≈_ Eq₂._≈_ to → - Congruent Eq₂._≈_ Eq₁._≈_ section - injective⇒to⁻-cong injective = section-cong + Congruent Eq₂._≈_ Eq₁._≈_ from + injective⇒to⁻-cong injective = from-cong where SB : Bijection S T SB = record { cong = cong ; bijective = injective , surjective } open Bijection (Symmetry.bijectionWithoutCongruence SB) - using () renaming (cong to section-cong) + using () renaming (cong to from-cong) {-# WARNING_ON_USAGE injective⇒to⁻-cong "Warning: injective⇒to⁻-cong was deprecated in v2.3. Please use Function.Construct.Symmetry.bijectionWithoutCongruence instead. " diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index 175bc1ac34..92814f014a 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -60,28 +60,28 @@ record IsInjection (to : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where open IsCongruent isCongruent public -record IsSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where +record IsSurjection (to : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field - isCongruent : IsCongruent f - surjective : Surjective _≈₁_ _≈₂_ f + isCongruent : IsCongruent to + surjective : Surjective _≈₁_ _≈₂_ to open IsCongruent isCongruent public open Section Eq₁.setoid Eq₂.setoid surjective public - using (section; inverseˡ; strictlyInverseˡ; strictlySurjective) + using (from; inverseˡ; strictlyInverseˡ; strictlySurjective) -record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where +record IsBijection (to : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field - isInjection : IsInjection f - surjective : Surjective _≈₁_ _≈₂_ f + isInjection : IsInjection to + surjective : Surjective _≈₁_ _≈₂_ to open IsInjection isInjection public - bijective : Bijective _≈₁_ _≈₂_ f + bijective : Bijective _≈₁_ _≈₂_ to bijective = injective , surjective - isSurjection : IsSurjection f + isSurjection : IsSurjection to isSurjection = record { isCongruent = isCongruent ; surjective = surjective @@ -90,12 +90,12 @@ record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where private module S = Section Eq₁.setoid Eq₂.setoid surjective open S public - using (strictlySurjective; section; inverseˡ; strictlyInverseˡ) + using (strictlySurjective; from; inverseˡ; strictlyInverseˡ) - inverseʳ : Inverseʳ _≈₁_ _≈₂_ f section + inverseʳ : Inverseʳ _≈₁_ _≈₂_ to from inverseʳ = S.inverseʳ injective - strictlyInverseʳ : StrictlyInverseʳ _≈₁_ f section + strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from strictlyInverseʳ = S.strictlyInverseʳ injective From 519980ff86c8dc776576b8812cde1b047a708060 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 6 Feb 2025 20:04:09 +0000 Subject: [PATCH 52/64] refactor: rename `f` to `to` for consistency --- src/Function/Structures.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index 92814f014a..0cb62011d3 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -201,9 +201,9 @@ record IsBiInverse -- See the comment on `SplitSurjection` in `Function.Bundles` for an -- explanation of (split) surjections. -record IsSplitSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where +record IsSplitSurjection (to : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field from : B → A - isLeftInverse : IsLeftInverse f from + isLeftInverse : IsLeftInverse to from open IsLeftInverse isLeftInverse public From 0e4e6c065f3cd27f475280f03137184aeb421104 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 6 Feb 2025 20:04:51 +0000 Subject: [PATCH 53/64] fix: comment on `SplitSurjection` --- src/Function/Bundles.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index 544240671a..05f655a909 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -399,7 +399,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where -- function for elements `x₁` and `x₂` are equal if `x₁ ≈ x₂` . -- -- The difference is the `from-cong` law --- generally, the section - -- (called `Surjection.to⁻` or `SplitSurjection.from`) of a surjection + -- (called `Surjection.from` or `SplitSurjection.from`) of a surjection -- need not respect equality, whereas it must in a split surjection. -- -- The two notions coincide when the equivalence relation on `B` is From d494fc9498b7fa3c27e16e720fcd3d5a0e9bf51c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 7 Feb 2025 08:01:53 +0000 Subject: [PATCH 54/64] refactor: fix names; inline definitions and use of the `Properties` --- src/Function/Construct/Symmetry.agda | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Function/Construct/Symmetry.agda b/src/Function/Construct/Symmetry.agda index 6a7ec8543e..810b058aa4 100644 --- a/src/Function/Construct/Symmetry.agda +++ b/src/Function/Construct/Symmetry.agda @@ -8,8 +8,8 @@ module Function.Construct.Symmetry where -open import Data.Product.Base using (_,_; swap; proj₁; proj₂) -open import Function.Base using (_∘_) +open import Data.Product.Base using (_,_; swap) +open import Function.Base using (_∘_; id) open import Function.Consequences using (module Section) open import Function.Definitions @@ -36,19 +36,19 @@ private module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) {f : A → B} {f⁻¹ : B → A} where inverseʳ : Inverseˡ ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₂ ≈₁ f⁻¹ f - inverseʳ inv = inv + inverseʳ = id inverseˡ : Inverseʳ ≈₁ ≈₂ f f⁻¹ → Inverseˡ ≈₂ ≈₁ f⁻¹ f - inverseˡ inv = inv + inverseˡ = id inverseᵇ : Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Inverseᵇ ≈₂ ≈₁ f⁻¹ f - inverseᵇ (invˡ , invʳ) = (invʳ , invˡ) + inverseᵇ = swap ------------------------------------------------------------------------ -- Structures -module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} - (isBij : IsBijection ≈₁ ≈₂ f) +module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {to : A → B} + (isBij : IsBijection ≈₁ ≈₂ to) where private module B = IsBijection isBij @@ -81,7 +81,7 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} {f⁻¹ : isLeftInverse inv = record { isCongruent = isCongruent F.isCongruent F.from-cong ; from-cong = F.to-cong - ; inverseˡ = inverseˡ ≈₁ ≈₂ F.inverseʳ + ; inverseˡ = F.inverseʳ } where module F = IsRightInverse inv isRightInverse : IsLeftInverse ≈₁ ≈₂ f f⁻¹ → IsRightInverse ≈₂ ≈₁ f⁻¹ f @@ -94,7 +94,7 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} {f⁻¹ : isInverse : IsInverse ≈₁ ≈₂ f f⁻¹ → IsInverse ≈₂ ≈₁ f⁻¹ f isInverse f-inv = record { isLeftInverse = isLeftInverse F.isRightInverse - ; inverseʳ = inverseʳ ≈₁ ≈₂ F.inverseˡ + ; inverseʳ = F.inverseˡ } where module F = IsInverse f-inv ------------------------------------------------------------------------ From 680f750376e0d490a6adaa82975241a7929f4155 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 7 Feb 2025 08:02:35 +0000 Subject: [PATCH 55/64] fix: names --- CHANGELOG.md | 44 ++++++++++++++++++++++---------------------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b5320d9b52..ee9ed75451 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,9 +7,9 @@ Highlights ---------- * A major overhaul of the `Function` hierarchy sees the systematic development - and use of theory of the left inverse to a given `Surjective` function `f`, in - `Function.Consequences.Section`, up to and including full symmetry of `Bijection`, in - `Function.Properties.Bijection`. + and use of theory of the left inverse `from` to a given `Surjective` function + `to`, in `Function.Consequences.Section`, up to and including full symmetry of + `Bijection`, in `Function.Properties.Bijection`. Bug-fixes --------- @@ -66,7 +66,7 @@ Deprecated names * In `Function.Bundles.IsSurjection`: ```agda - to⁻ ↦ Function.Structures.IsSurjection.section + to⁻ ↦ Function.Structures.IsSurjection.from to∘to⁻ ↦ Function.Structures.IsSurjection.strictlyInverseˡ ``` @@ -129,11 +129,11 @@ Additions to existing modules * In `Function.Bundles.Bijection`: ```agda - section : B → A - inverseˡ : Inverseˡ _≈₁_ _≈₂_ to section - strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to section - inverseʳ : Inverseʳ _≈₁_ _≈₂_ to section - strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to section + from : B → A + inverseˡ : Inverseˡ _≈₁_ _≈₂_ to from + strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from + inverseʳ : Inverseʳ _≈₁_ _≈₂_ to from + strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from ``` * In `Function.Bundles.LeftInverse`: @@ -151,20 +151,20 @@ Additions to existing modules * In `Function.Bundles.Surjection`: ```agda - section : B → A - inverseˡ : Inverseˡ _≈₁_ _≈₂_ to section - strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to section + from : B → A + inverseˡ : Inverseˡ _≈₁_ _≈₂_ to from + strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from ``` * In `Function.Consequences` and `Function.Consequences.Setoid`: the theory of the left inverse of a surjective function ```agda - module Section (surj : Surjective ≈₁ ≈₂ f) + module Section (surj : Surjective ≈₁ ≈₂ to) ``` * In `Function.Construct.Symmetry`: ```agda - isBijectionWithoutCongruence : (IsBijection ≈₁ ≈₂ f) → IsBijection ≈₂ ≈₁ section + isBijectionWithoutCongruence : (IsBijection ≈₁ ≈₂ to) → IsBijection ≈₂ ≈₁ from bijectionWithoutCongruence : (Bijection R S) → Bijection S R ``` @@ -175,11 +175,11 @@ Additions to existing modules * In `Function.Structures.IsBijection`: ```agda - section : B → A - inverseˡ : Inverseˡ _≈₁_ _≈₂_ f section - strictlyInverseˡ : StrictlyInverseˡ _≈₂_ f section - inverseʳ : Inverseʳ _≈₁_ _≈₂_ f section - strictlyInverseʳ : StrictlyInverseʳ _≈₁_ f section + from : B → A + inverseˡ : Inverseˡ _≈₁_ _≈₂_ to from + strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from + inverseʳ : Inverseʳ _≈₁_ _≈₂_ to from + strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from ``` * In `Function.Structures.IsLeftInverse`: @@ -195,8 +195,8 @@ Additions to existing modules * In `Function.Structures.IsSurjection`: ```agda - section : B → A - inverseˡ : Inverseˡ _≈₁_ _≈₂_ f section - strictlyInverseˡ : StrictlyInverseˡ _≈₂_ f section + from : B → A + inverseˡ : Inverseˡ _≈₁_ _≈₂_ to from + strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from ``` From e72c9e765e5ab05f6da651ff7b64fda2b5ada6d8 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 7 Feb 2025 08:05:35 +0000 Subject: [PATCH 56/64] fix: parentheses --- CHANGELOG.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index ee9ed75451..f4cd26269b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -157,15 +157,15 @@ Additions to existing modules ``` * In `Function.Consequences` and `Function.Consequences.Setoid`: - the theory of the left inverse of a surjective function + the theory of the left inverse of a surjective function `to` ```agda module Section (surj : Surjective ≈₁ ≈₂ to) ``` * In `Function.Construct.Symmetry`: ```agda - isBijectionWithoutCongruence : (IsBijection ≈₁ ≈₂ to) → IsBijection ≈₂ ≈₁ from - bijectionWithoutCongruence : (Bijection R S) → Bijection S R + isBijectionWithoutCongruence : IsBijection ≈₁ ≈₂ to → IsBijection ≈₂ ≈₁ from + bijectionWithoutCongruence : Bijection R S → Bijection S R ``` * In `Function.Properties.Bijection`: From 62a15739ac125e16e6626aa9653265787e0c7297 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 7 Feb 2025 08:11:38 +0000 Subject: [PATCH 57/64] fix: names --- src/Data/Product/Function/Dependent/Propositional.agda | 6 +++--- src/Data/Product/Function/Dependent/Setoid.agda | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Data/Product/Function/Dependent/Propositional.agda b/src/Data/Product/Function/Dependent/Propositional.agda index 7008117ede..ba9db6fb6e 100644 --- a/src/Data/Product/Function/Dependent/Propositional.agda +++ b/src/Data/Product/Function/Dependent/Propositional.agda @@ -196,11 +196,11 @@ module _ where backcast : ∀ {i} → B i → B (to I↠J (from I↠J i)) backcast = ≡.subst B (≡.sym (strictlyInverseˡ I↠J _)) - section′ : Σ J B → Σ I A - section′ = map (from I↠J) (from A↠B ∘ backcast) + from′ : Σ J B → Σ I A + from′ = map (from I↠J) (from A↠B ∘ backcast) strictlySurjective′ : StrictlySurjective _≡_ to′ - strictlySurjective′ (x , y) = section′ (x , y) , Σ-≡,≡→≡ + strictlySurjective′ (x , y) = from′ (x , y) , Σ-≡,≡→≡ ( strictlyInverseˡ I↠J x , (begin ≡.subst B (strictlyInverseˡ I↠J x) (to A↠B (from A↠B (backcast y))) diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda index 2303230da5..671b219a54 100644 --- a/src/Data/Product/Function/Dependent/Setoid.agda +++ b/src/Data/Product/Function/Dependent/Setoid.agda @@ -171,11 +171,11 @@ module _ where func : Func (I ×ₛ A) (J ×ₛ B) func = function (Surjection.function I↠J) (Surjection.function A↠B) - section′ : Carrier (J ×ₛ B) → Carrier (I ×ₛ A) - section′ (j , y) = from I↠J j , from A↠B (cast B (strictlyInverseˡ I↠J _) y) + from′ : Carrier (J ×ₛ B) → Carrier (I ×ₛ A) + from′ (j , y) = from I↠J j , from A↠B (cast B (strictlyInverseˡ I↠J _) y) strictlySurj : StrictlySurjective (Func.Eq₂._≈_ func) (Func.to func) - strictlySurj (j , y) = section′ (j , y) , + strictlySurj (j , y) = from′ (j , y) , strictlyInverseˡ I↠J j , IndexedSetoid.trans B (strictlyInverseˡ A↠B _) (cast-eq B (strictlyInverseˡ I↠J j)) surj : Surjective (Func.Eq₁._≈_ func) (Func.Eq₂._≈_ func) (Func.to func) From ea2eb998eef4d2882d8a241e6365b209e07ba921 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 7 Feb 2025 08:36:12 +0000 Subject: [PATCH 58/64] fix: tighten imports --- src/Function/Bundles.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index 05f655a909..da22fdd763 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -21,6 +21,7 @@ module Function.Bundles where open import Function.Base using (_∘_) open import Function.Consequences.Propositional + using (strictlySurjective⇒surjective; strictlyInverseˡ⇒inverseˡ; strictlyInverseʳ⇒inverseʳ) open import Function.Definitions import Function.Structures as FunctionStructures open import Level using (Level; _⊔_; suc) From c8a6e5a2d853fcb8d8f684195f6a8becff5ee9e4 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 8 Feb 2025 19:14:28 +0000 Subject: [PATCH 59/64] =?UTF-8?q?fix:=20`variable`s,=20specifically=20`f?= =?UTF-8?q?=E2=81=BB=C2=B9`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Function/Consequences.agda | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda index 8e77e8b03d..d31766e55a 100644 --- a/src/Function/Consequences.agda +++ b/src/Function/Consequences.agda @@ -24,7 +24,9 @@ private a b ℓ₁ ℓ₂ : Level A B : Set a ≈₁ ≈₂ : Rel A ℓ₁ - to f f⁻¹ : A → B + to f : A → B + f⁻¹ : B → A + ------------------------------------------------------------------------ -- Injective From 3e378546cacc3df7a91c1840a0d29e6e86314485 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 8 Feb 2025 19:15:04 +0000 Subject: [PATCH 60/64] fix: cosmetics --- src/Function/Consequences/Setoid.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Function/Consequences/Setoid.agda b/src/Function/Consequences/Setoid.agda index 98669b0606..36785aee7a 100644 --- a/src/Function/Consequences/Setoid.agda +++ b/src/Function/Consequences/Setoid.agda @@ -28,6 +28,7 @@ private to f : A → B f⁻¹ : B → A + ------------------------------------------------------------------------ -- Injective From dfe1bf16029876fe97815276e9f14e90df8eb821 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 8 Feb 2025 19:32:38 +0000 Subject: [PATCH 61/64] refactor: PROVISIONAL; show the effect of inlining --- src/Function/Consequences/Propositional.agda | 33 ++++++++++++++------ 1 file changed, 23 insertions(+), 10 deletions(-) diff --git a/src/Function/Consequences/Propositional.agda b/src/Function/Consequences/Propositional.agda index a2558a9c48..2fbb4155be 100644 --- a/src/Function/Consequences/Propositional.agda +++ b/src/Function/Consequences/Propositional.agda @@ -11,14 +11,20 @@ module Function.Consequences.Propositional {a b} {A : Set a} {B : Set b} where -open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; cong) +open import Data.Product.Base using (_,_) +open import Function.Definitions +open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) open import Relation.Binary.PropositionalEquality.Properties using (setoid) -open import Function.Definitions -open import Relation.Nullary.Negation.Core using (contraposition) import Function.Consequences.Setoid (setoid A) (setoid B) as Setoid +private + variable + f : A → B + f⁻¹ : B → A + + ------------------------------------------------------------------------ -- Re-export setoid properties @@ -32,22 +38,29 @@ open Setoid public ------------------------------------------------------------------------ -- Properties that rely on congruence -private - variable - f : A → B - f⁻¹ : B → A - strictlySurjective⇒surjective : StrictlySurjective _≡_ f → Surjective _≡_ _≡_ f +strictlySurjective⇒surjective strict y = + let (x , fx≡y) = strict y in x , λ where refl → fx≡y +{- strictlySurjective⇒surjective = Setoid.strictlySurjective⇒surjective (cong _) +-} strictlyInverseˡ⇒inverseˡ : ∀ f → StrictlyInverseˡ _≡_ f f⁻¹ → Inverseˡ _≡_ _≡_ f f⁻¹ -strictlyInverseˡ⇒inverseˡ f = +strictlyInverseˡ⇒inverseˡ f strict refl = strict _ +{- +strictlyInverseˡ⇒inverseˡ = Setoid.strictlyInverseˡ⇒inverseˡ (cong _) +-} + strictlyInverseʳ⇒inverseʳ : ∀ f → StrictlyInverseʳ _≡_ f f⁻¹ → Inverseʳ _≡_ _≡_ f f⁻¹ -strictlyInverseʳ⇒inverseʳ f = +strictlyInverseʳ⇒inverseʳ f strict refl = strict _ +{- +strictlyInverseʳ⇒inverseʳ = strict _ Setoid.strictlyInverseʳ⇒inverseʳ (cong _) +-} + From a6883ffce50b724101e6cca40fa9d13317f87795 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 8 Feb 2025 19:37:15 +0000 Subject: [PATCH 62/64] fix_ whitespace --- src/Function/Consequences/Propositional.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Function/Consequences/Propositional.agda b/src/Function/Consequences/Propositional.agda index 2fbb4155be..59fc1705e9 100644 --- a/src/Function/Consequences/Propositional.agda +++ b/src/Function/Consequences/Propositional.agda @@ -49,7 +49,7 @@ strictlySurjective⇒surjective = strictlyInverseˡ⇒inverseˡ : ∀ f → StrictlyInverseˡ _≡_ f f⁻¹ → Inverseˡ _≡_ _≡_ f f⁻¹ -strictlyInverseˡ⇒inverseˡ f strict refl = strict _ +strictlyInverseˡ⇒inverseˡ f strict refl = strict _ {- strictlyInverseˡ⇒inverseˡ = Setoid.strictlyInverseˡ⇒inverseˡ (cong _) @@ -63,4 +63,4 @@ strictlyInverseʳ⇒inverseʳ f strict refl = strict _ strictlyInverseʳ⇒inverseʳ = strict _ Setoid.strictlyInverseʳ⇒inverseʳ (cong _) -} - + From 098d0a3adf7ef8cadea1942fe4e56f19cacf81b9 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 9 Feb 2025 06:10:41 +0000 Subject: [PATCH 63/64] refactor: tidy up --- src/Function/Consequences/Propositional.agda | 22 ++++---------------- 1 file changed, 4 insertions(+), 18 deletions(-) diff --git a/src/Function/Consequences/Propositional.agda b/src/Function/Consequences/Propositional.agda index 59fc1705e9..17d665e898 100644 --- a/src/Function/Consequences/Propositional.agda +++ b/src/Function/Consequences/Propositional.agda @@ -40,27 +40,13 @@ open Setoid public strictlySurjective⇒surjective : StrictlySurjective _≡_ f → Surjective _≡_ _≡_ f -strictlySurjective⇒surjective strict y = - let (x , fx≡y) = strict y in x , λ where refl → fx≡y -{- -strictlySurjective⇒surjective = - Setoid.strictlySurjective⇒surjective (cong _) --} +strictlySurjective⇒surjective surj y = + let x , fx≡y = surj y in x , λ where refl → fx≡y strictlyInverseˡ⇒inverseˡ : ∀ f → StrictlyInverseˡ _≡_ f f⁻¹ → Inverseˡ _≡_ _≡_ f f⁻¹ -strictlyInverseˡ⇒inverseˡ f strict refl = strict _ -{- -strictlyInverseˡ⇒inverseˡ = - Setoid.strictlyInverseˡ⇒inverseˡ (cong _) --} - +strictlyInverseˡ⇒inverseˡ _ inv refl = inv _ strictlyInverseʳ⇒inverseʳ : ∀ f → StrictlyInverseʳ _≡_ f f⁻¹ → Inverseʳ _≡_ _≡_ f f⁻¹ -strictlyInverseʳ⇒inverseʳ f strict refl = strict _ -{- -strictlyInverseʳ⇒inverseʳ = strict _ - Setoid.strictlyInverseʳ⇒inverseʳ (cong _) --} - +strictlyInverseʳ⇒inverseʳ _ inv refl = inv _ From 2aa18061ba39faac235cc6655d52f62f8d15d5ff Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 9 Feb 2025 09:35:26 +0000 Subject: [PATCH 64/64] refactor: rename `Sf` to `From` --- src/Function/Consequences/Setoid.agda | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/Function/Consequences/Setoid.agda b/src/Function/Consequences/Setoid.agda index 36785aee7a..e2237f4fff 100644 --- a/src/Function/Consequences/Setoid.agda +++ b/src/Function/Consequences/Setoid.agda @@ -97,32 +97,32 @@ strictlyInverseʳ⇒inverseʳ = C.strictlyInverseʳ⇒inverseʳ S.trans module Section (surj : Surjective ≈₁ ≈₂ to) where - private module Sf = C.Section ≈₂ surj + private module From = C.Section ≈₂ surj - open Sf public using (from; inverseˡ) + open From public using (from; inverseˡ) strictlySurjective : StrictlySurjective ≈₂ to - strictlySurjective = Sf.strictlySurjective S.refl + strictlySurjective = From.strictlySurjective S.refl strictlyInverseˡ : StrictlyInverseˡ ≈₂ to from - strictlyInverseˡ = Sf.strictlyInverseˡ S.refl + strictlyInverseˡ = From.strictlyInverseˡ S.refl injective : Injective ≈₂ ≈₁ from - injective = Sf.injective S.refl T.sym T.trans + injective = From.injective S.refl T.sym T.trans module _ (inj : Injective ≈₁ ≈₂ to) where cong : Congruent ≈₂ ≈₁ from - cong = Sf.cong inj S.refl T.sym T.trans + cong = From.cong inj S.refl T.sym T.trans inverseʳ : Inverseʳ ≈₁ ≈₂ to from - inverseʳ = Sf.inverseʳ inj S.refl T.trans + inverseʳ = From.inverseʳ inj S.refl T.trans strictlyInverseʳ : StrictlyInverseʳ ≈₁ to from - strictlyInverseʳ = Sf.strictlyInverseʳ inj S.refl T.refl T.trans + strictlyInverseʳ = From.strictlyInverseʳ inj S.refl T.refl T.trans surjective : Surjective ≈₂ ≈₁ from - surjective = Sf.surjective inj S.refl T.trans + surjective = From.surjective inj S.refl T.trans bijective : Bijective ≈₂ ≈₁ from - bijective = Sf.bijective inj S.refl T.sym T.trans + bijective = From.bijective inj S.refl T.sym T.trans