From 9a712000ee56de8d3bfecc268082bd6a176a6a3f Mon Sep 17 00:00:00 2001 From: Alex Rice Date: Thu, 16 Apr 2020 17:07:44 +0100 Subject: [PATCH 1/4] Change to using strict inverses --- src/Function/Construct/Composition.agda | 54 +++++++++++-------------- src/Function/Construct/Identity.agda | 40 +++++++++--------- src/Function/Definitions.agda | 12 +++--- 3 files changed, 50 insertions(+), 56 deletions(-) diff --git a/src/Function/Construct/Composition.agda b/src/Function/Construct/Composition.agda index ae8cbd09b7..e2b3205477 100644 --- a/src/Function/Construct/Composition.agda +++ b/src/Function/Construct/Composition.agda @@ -35,39 +35,33 @@ module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) (≈₃ : Rel C ℓ₃) Injective ≈₁ ≈₃ (g ∘ f) injective f-inj g-inj = f-inj ∘ g-inj - surjective : Transitive ≈₃ → Congruent ≈₂ ≈₃ g → - Surjective ≈₁ ≈₂ f → Surjective ≈₂ ≈₃ g → + surjective : Surjective ≈₁ ≈₂ f → Surjective ≈₂ ≈₃ g → Surjective ≈₁ ≈₃ (g ∘ f) - surjective trans g-cong f-sur g-sur x with g-sur x - ... | y , fy≈x with f-sur y - ... | z , fz≈y = z , trans (g-cong fz≈y) fy≈x + surjective f-sur g-sur x with g-sur x + ... | y , gproof with f-sur y + ... | z , fproof = z , λ a a≈z → gproof (f a) (fproof a a≈z) - bijective : Transitive ≈₃ → Congruent ≈₂ ≈₃ g → - Bijective ≈₁ ≈₂ f → Bijective ≈₂ ≈₃ g → + bijective : Bijective ≈₁ ≈₂ f → Bijective ≈₂ ≈₃ g → Bijective ≈₁ ≈₃ (g ∘ f) - bijective trans g-cong (f-inj , f-sur) (g-inj , g-sur) = - injective f-inj g-inj , surjective trans g-cong f-sur g-sur + bijective (f-inj , f-sur) (g-inj , g-sur) = + injective f-inj g-inj , surjective f-sur g-sur module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) (≈₃ : Rel C ℓ₃) (f : A → B) {f⁻¹ : B → A} {g : B → C} (g⁻¹ : C → B) where - inverseˡ : Transitive ≈₃ → Congruent ≈₂ ≈₃ g → - Inverseˡ ≈₁ ≈₂ f f⁻¹ → Inverseˡ ≈₂ ≈₃ g g⁻¹ → + inverseˡ : Inverseˡ ≈₁ ≈₂ f f⁻¹ → Inverseˡ ≈₂ ≈₃ g g⁻¹ → Inverseˡ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹) - inverseˡ trn g-cong f-inv g-inv x = trn (g-cong (f-inv _)) (g-inv x) + inverseˡ f-inv g-inv x y y≈gfx = g-inv x (f y) (f-inv (g⁻¹ x) y y≈gfx) - inverseʳ : Transitive ≈₁ → Congruent ≈₂ ≈₁ f⁻¹ → - Inverseʳ ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₂ ≈₃ g g⁻¹ → + inverseʳ : Inverseʳ ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₂ ≈₃ g g⁻¹ → Inverseʳ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹) - inverseʳ trn f⁻¹-cong f-inv g-inv x = trn (f⁻¹-cong (g-inv _)) (f-inv x) + inverseʳ f-inv g-inv x y y≈gfx = f-inv x (g⁻¹ y) (g-inv (f x) y y≈gfx) - inverseᵇ : Transitive ≈₁ → Transitive ≈₃ → - Congruent ≈₂ ≈₃ g → Congruent ≈₂ ≈₁ f⁻¹ → - Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Inverseᵇ ≈₂ ≈₃ g g⁻¹ → + inverseᵇ : Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Inverseᵇ ≈₂ ≈₃ g g⁻¹ → Inverseᵇ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹) - inverseᵇ trn₁ trn₃ g-cong f⁻¹-cong (f-invˡ , f-invʳ) (g-invˡ , g-invʳ) = - inverseˡ trn₃ g-cong f-invˡ g-invˡ , inverseʳ trn₁ f⁻¹-cong f-invʳ g-invʳ + inverseᵇ (f-invˡ , f-invʳ) (g-invˡ , g-invʳ) = + inverseˡ f-invˡ g-invˡ , inverseʳ f-invʳ g-invʳ ------------------------------------------------------------------------ -- Structures @@ -95,14 +89,14 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {≈₃ : Rel C ℓ₃} IsSurjection ≈₁ ≈₃ (g ∘ f) isSurjection f-surj g-surj = record { isCongruent = isCongruent F.isCongruent G.isCongruent - ; surjective = surjective ≈₁ ≈₂ ≈₃ G.Eq₂.trans G.cong F.surjective G.surjective + ; surjective = surjective ≈₁ ≈₂ ≈₃ F.surjective G.surjective } where module F = IsSurjection f-surj; module G = IsSurjection g-surj isBijection : IsBijection ≈₁ ≈₂ f → IsBijection ≈₂ ≈₃ g → IsBijection ≈₁ ≈₃ (g ∘ f) isBijection f-bij g-bij = record { isInjection = isInjection F.isInjection G.isInjection - ; surjective = surjective ≈₁ ≈₂ ≈₃ G.Eq₂.trans G.cong F.surjective G.surjective + ; surjective = surjective ≈₁ ≈₂ ≈₃ F.surjective G.surjective } where module F = IsBijection f-bij; module G = IsBijection g-bij module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {≈₃ : Rel C ℓ₃} @@ -114,7 +108,7 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {≈₃ : Rel C ℓ₃} isLeftInverse f-invˡ g-invˡ = record { isCongruent = isCongruent F.isCongruent G.isCongruent ; cong₂ = congruent ≈₃ ≈₂ ≈₁ G.cong₂ F.cong₂ - ; inverseˡ = inverseˡ ≈₁ ≈₂ ≈₃ f _ G.Eq₂.trans G.cong₁ F.inverseˡ G.inverseˡ + ; inverseˡ = inverseˡ ≈₁ ≈₂ ≈₃ f _ F.inverseˡ G.inverseˡ } where module F = IsLeftInverse f-invˡ; module G = IsLeftInverse g-invˡ isRightInverse : IsRightInverse ≈₁ ≈₂ f f⁻¹ → IsRightInverse ≈₂ ≈₃ g g⁻¹ → @@ -122,14 +116,14 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {≈₃ : Rel C ℓ₃} isRightInverse f-invʳ g-invʳ = record { isCongruent = isCongruent F.isCongruent G.isCongruent ; cong₂ = congruent ≈₃ ≈₂ ≈₁ G.cong₂ F.cong₂ - ; inverseʳ = inverseʳ ≈₁ ≈₂ ≈₃ _ g⁻¹ F.Eq₁.trans F.cong₂ F.inverseʳ G.inverseʳ + ; inverseʳ = inverseʳ ≈₁ ≈₂ ≈₃ _ g⁻¹ F.inverseʳ G.inverseʳ } where module F = IsRightInverse f-invʳ; module G = IsRightInverse g-invʳ isInverse : IsInverse ≈₁ ≈₂ f f⁻¹ → IsInverse ≈₂ ≈₃ g g⁻¹ → IsInverse ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹) isInverse f-inv g-inv = record { isLeftInverse = isLeftInverse F.isLeftInverse G.isLeftInverse - ; inverseʳ = inverseʳ ≈₁ ≈₂ ≈₃ _ g⁻¹ F.Eq₁.trans F.cong₂ F.inverseʳ G.inverseʳ + ; inverseʳ = inverseʳ ≈₁ ≈₂ ≈₃ _ g⁻¹ F.inverseʳ G.inverseʳ } where module F = IsInverse f-inv; module G = IsInverse g-inv ------------------------------------------------------------------------ @@ -150,14 +144,14 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} {T : Setoid c ℓ₃} where surjection surj₁ surj₂ = record { f = G.f ∘ F.f ; cong = congruent (≈ R) (≈ S) (≈ T) F.cong G.cong - ; surjective = surjective (≈ R) (≈ S) (≈ T) G.Eq₂.trans G.cong F.surjective G.surjective + ; surjective = surjective (≈ R) (≈ S) (≈ T) F.surjective G.surjective } where module F = Surjection surj₁; module G = Surjection surj₂ bijection : Bijection R S → Bijection S T → Bijection R T bijection bij₁ bij₂ = record { f = G.f ∘ F.f ; cong = congruent (≈ R) (≈ S) (≈ T) F.cong G.cong - ; bijective = bijective (≈ R) (≈ S) (≈ T) (trans T) G.cong F.bijective G.bijective + ; bijective = bijective (≈ R) (≈ S) (≈ T) F.bijective G.bijective } where module F = Bijection bij₁; module G = Bijection bij₂ equivalence : Equivalence R S → Equivalence S T → Equivalence R T @@ -174,7 +168,7 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} {T : Setoid c ℓ₃} where ; g = F.g ∘ G.g ; cong₁ = congruent (≈ R) (≈ S) (≈ T) F.cong₁ G.cong₁ ; cong₂ = congruent (≈ T) (≈ S) (≈ R) G.cong₂ F.cong₂ - ; inverseˡ = inverseˡ (≈ R) (≈ S) (≈ T) F.f _ (trans T) G.cong₁ F.inverseˡ G.inverseˡ + ; inverseˡ = inverseˡ (≈ R) (≈ S) (≈ T) F.f _ F.inverseˡ G.inverseˡ } where module F = LeftInverse invˡ₁; module G = LeftInverse invˡ₂ rightInverse : RightInverse R S → RightInverse S T → RightInverse R T @@ -183,7 +177,7 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} {T : Setoid c ℓ₃} where ; g = F.g ∘ G.g ; cong₁ = congruent (≈ R) (≈ S) (≈ T) F.cong₁ G.cong₁ ; cong₂ = congruent (≈ T) (≈ S) (≈ R) G.cong₂ F.cong₂ - ; inverseʳ = inverseʳ (≈ R) (≈ S) (≈ T) _ G.g (trans R) F.cong₂ F.inverseʳ G.inverseʳ + ; inverseʳ = inverseʳ (≈ R) (≈ S) (≈ T) _ G.g F.inverseʳ G.inverseʳ } where module F = RightInverse invʳ₁; module G = RightInverse invʳ₂ inverse : Inverse R S → Inverse S T → Inverse R T @@ -192,7 +186,7 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} {T : Setoid c ℓ₃} where ; f⁻¹ = F.f⁻¹ ∘ G.f⁻¹ ; cong₁ = congruent (≈ R) (≈ S) (≈ T) F.cong₁ G.cong₁ ; cong₂ = congruent (≈ T) (≈ S) (≈ R) G.cong₂ F.cong₂ - ; inverse = inverseᵇ (≈ R) (≈ S) (≈ T) _ G.f⁻¹ (trans R) (trans T) G.cong₁ F.cong₂ F.inverse G.inverse + ; inverse = inverseᵇ (≈ R) (≈ S) (≈ T) _ G.f⁻¹ F.inverse G.inverse } where module F = Inverse inv₁; module G = Inverse inv₂ ------------------------------------------------------------------------ diff --git a/src/Function/Construct/Identity.agda b/src/Function/Construct/Identity.agda index 2207a57898..64aba15415 100644 --- a/src/Function/Construct/Identity.agda +++ b/src/Function/Construct/Identity.agda @@ -32,20 +32,20 @@ module _ (_≈_ : Rel A ℓ) where injective : Injective id injective = id - surjective : Reflexive _≈_ → Surjective id - surjective refl x = x , refl + surjective : Surjective id + surjective x = x , λ z z≈x → z≈x - bijective : Reflexive _≈_ → Bijective id - bijective refl = injective , surjective refl + bijective : Bijective id + bijective = injective , surjective - inverseˡ : Reflexive _≈_ → Inverseˡ id id - inverseˡ refl x = refl + inverseˡ : Inverseˡ id id + inverseˡ x y y≈x = y≈x - inverseʳ : Reflexive _≈_ → Inverseʳ id id - inverseʳ refl x = refl + inverseʳ : Inverseʳ id id + inverseʳ x y y≈x = y≈x - inverseᵇ : Reflexive _≈_ → Inverseᵇ id id - inverseᵇ refl = inverseˡ refl , inverseʳ refl + inverseᵇ : Inverseᵇ id id + inverseᵇ = inverseˡ , inverseʳ ------------------------------------------------------------------------ -- Structures @@ -71,33 +71,33 @@ module _ {_≈_ : Rel A ℓ} (isEq : IsEquivalence _≈_) where isSurjection : IsSurjection id isSurjection = record { isCongruent = isCongruent - ; surjective = surjective _≈_ refl + ; surjective = surjective _≈_ } isBijection : IsBijection id isBijection = record { isInjection = isInjection - ; surjective = surjective _≈_ refl + ; surjective = surjective _≈_ } isLeftInverse : IsLeftInverse id id isLeftInverse = record { isCongruent = isCongruent ; cong₂ = id - ; inverseˡ = inverseˡ _≈_ refl + ; inverseˡ = inverseˡ _≈_ } isRightInverse : IsRightInverse id id isRightInverse = record { isCongruent = isCongruent ; cong₂ = id - ; inverseʳ = inverseʳ _≈_ refl + ; inverseʳ = inverseʳ _≈_ } isInverse : IsInverse id id isInverse = record { isLeftInverse = isLeftInverse - ; inverseʳ = inverseʳ _≈_ refl + ; inverseʳ = inverseʳ _≈_ } ------------------------------------------------------------------------ @@ -118,14 +118,14 @@ module _ (S : Setoid a ℓ) where surjection = record { f = id ; cong = id - ; surjective = surjective _≈_ refl + ; surjective = surjective _≈_ } bijection : Bijection S S bijection = record { f = id ; cong = id - ; bijective = bijective _≈_ refl + ; bijective = bijective _≈_ } equivalence : Equivalence S S @@ -142,7 +142,7 @@ module _ (S : Setoid a ℓ) where ; g = id ; cong₁ = id ; cong₂ = id - ; inverseˡ = inverseˡ _≈_ refl + ; inverseˡ = inverseˡ _≈_ } rightInverse : RightInverse S S @@ -151,7 +151,7 @@ module _ (S : Setoid a ℓ) where ; g = id ; cong₁ = id ; cong₂ = id - ; inverseʳ = inverseʳ _≈_ refl + ; inverseʳ = inverseʳ _≈_ } inverse : Inverse S S @@ -160,7 +160,7 @@ module _ (S : Setoid a ℓ) where ; f⁻¹ = id ; cong₁ = id ; cong₂ = id - ; inverse = inverseᵇ _≈_ refl + ; inverse = inverseᵇ _≈_ } ------------------------------------------------------------------------ diff --git a/src/Function/Definitions.agda b/src/Function/Definitions.agda index 2c139cf318..f3cd82fd0b 100644 --- a/src/Function/Definitions.agda +++ b/src/Function/Definitions.agda @@ -30,17 +30,17 @@ Congruent f = ∀ {x y} → x ≈₁ y → f x ≈₂ f y Injective : (A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂) Injective f = ∀ {x y} → f x ≈₂ f y → x ≈₁ y -open Core₂ _≈₂_ public - using (Surjective) +Surjective : (A → B) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) +Surjective f = ∀ y → ∃ λ x → ∀ z → z ≈₁ x → f z ≈₂ y Bijective : (A → B) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) Bijective f = Injective f × Surjective f -open Core₂ _≈₂_ public - using (Inverseˡ) +Inverseˡ : (A → B) → (B → A) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) +Inverseˡ f g = ∀ x y → y ≈₁ g x → f y ≈₂ x -open Core₁ _≈₁_ public - using (Inverseʳ) +Inverseʳ : (A → B) → (B → A) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) +Inverseʳ f g = ∀ x y → y ≈₂ f x → g y ≈₁ x Inverseᵇ : (A → B) → (B → A) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) Inverseᵇ f g = Inverseˡ f g × Inverseʳ f g From b8db0b46a7b347c5d6f0c2110e1fc41fbdad71f8 Mon Sep 17 00:00:00 2001 From: = Date: Sat, 12 Mar 2022 20:43:47 +0000 Subject: [PATCH 2/4] Fix whitespace --- 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 ca92015b6d..6038ef43ec 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -100,7 +100,7 @@ record IsLeftInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ open IsCongruent isCongruent public renaming (cong to to-cong) - + strictInverseˡ : ∀ x → to (from x) ≈₂ x strictInverseˡ x = inverseˡ x Eq₁.refl From 96aaa6e2eeb9fbc4b4e38aaa4591426b83655b4d Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Tue, 6 Jun 2023 20:28:18 +0900 Subject: [PATCH 3/4] Pushed changes all the way through --- src/Algebra/Consequences/Setoid.agda | 37 ++---- .../Morphism/Construct/Composition.agda | 2 +- .../Lattice/Morphism/Construct/Identity.agda | 3 +- src/Algebra/Lattice/Morphism/Structures.agda | 7 +- .../Morphism/Construct/Composition.agda | 16 +-- .../Module/Morphism/Construct/Identity.agda | 17 +-- src/Algebra/Module/Morphism/Structures.agda | 42 +++--- src/Algebra/Morphism/Consequences.agda | 14 +- .../Morphism/Construct/Composition.agda | 18 +-- src/Algebra/Morphism/Construct/Identity.agda | 19 +-- src/Algebra/Morphism/Structures.agda | 47 +++---- src/Data/Fin/Permutation.agda | 20 +-- src/Data/Fin/Properties.agda | 17 ++- .../Sublist/Heterogeneous/Properties.agda | 4 +- .../Unary/Enumerates/Setoid/Properties.agda | 12 +- src/Data/Nat/Binary/Properties.agda | 17 ++- src/Data/Nat/Binary/Subtraction.agda | 4 +- src/Data/Parity/Properties.agda | 19 ++- src/Data/Product/Algebra.agda | 12 +- src/Data/Sum/Algebra.agda | 13 +- src/Data/Vec/N-ary.agda | 4 +- src/Data/Vec/Recursive.agda | 9 +- src/Function/Bundles.agda | 118 +++++++++-------- src/Function/Consequences.agda | 121 +++++++++++++----- src/Function/Consequences/Propositional.agda | 91 +++++++++++++ src/Function/Construct/Composition.agda | 4 +- src/Function/Construct/Identity.agda | 20 +-- src/Function/Definitions.agda | 62 ++++++--- src/Function/Properties.agda | 4 +- src/Function/Properties/Bijection.agda | 15 +-- src/Function/Properties/Inverse.agda | 12 +- src/Function/Properties/RightInverse.agda | 4 +- src/Function/Properties/Surjection.agda | 23 +++- src/Function/Related.agda | 20 +-- src/Function/Structures.agda | 13 +- .../Morphism/Construct/Composition.agda | 8 +- .../Binary/Morphism/Construct/Identity.agda | 11 +- 37 files changed, 527 insertions(+), 352 deletions(-) create mode 100644 src/Function/Consequences/Propositional.agda diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda index c51a6ee8b1..9055273b27 100644 --- a/src/Algebra/Consequences/Setoid.agda +++ b/src/Algebra/Consequences/Setoid.agda @@ -16,8 +16,8 @@ open import Algebra.Core open import Algebra.Definitions _≈_ open import Data.Sum.Base using (inj₁; inj₂) open import Data.Product using (_,_) -open import Function.Base using (_$_) -import Function.Definitions as FunDefs +open import Function.Base using (_$_; id; _∘_) +open import Function.Definitions import Relation.Binary.Consequences as Bin open import Relation.Binary.Reasoning.Setoid S open import Relation.Unary using (Pred) @@ -30,45 +30,32 @@ open import Relation.Unary using (Pred) open import Algebra.Consequences.Base public ------------------------------------------------------------------------ --- Involutive/SelfInverse functions - -module _ {f : Op₁ A} (inv : Involutive f) where - - open FunDefs _≈_ _≈_ - - involutive⇒surjective : Surjective f - involutive⇒surjective y = f y , inv y +-- SelfInverse functions module _ {f : Op₁ A} (self : SelfInverse f) where selfInverse⇒involutive : Involutive f selfInverse⇒involutive = reflexive+selfInverse⇒involutive _≈_ refl self - private - - inv = selfInverse⇒involutive - - open FunDefs _≈_ _≈_ - - selfInverse⇒congruent : Congruent f + selfInverse⇒congruent : Congruent _≈_ _≈_ f selfInverse⇒congruent {x} {y} x≈y = sym (self (begin - f (f x) ≈⟨ inv x ⟩ + f (f x) ≈⟨ selfInverse⇒involutive x ⟩ x ≈⟨ x≈y ⟩ y ∎)) - selfInverse⇒inverseᵇ : Inverseᵇ f f - selfInverse⇒inverseᵇ = inv , inv + selfInverse⇒inverseᵇ : Inverseᵇ _≈_ _≈_ f f + selfInverse⇒inverseᵇ = self ∘ sym , self ∘ sym - selfInverse⇒surjective : Surjective f - selfInverse⇒surjective = involutive⇒surjective inv + selfInverse⇒surjective : Surjective _≈_ _≈_ f + selfInverse⇒surjective y = f y , self ∘ sym - selfInverse⇒injective : Injective f + selfInverse⇒injective : Injective _≈_ _≈_ f selfInverse⇒injective {x} {y} x≈y = begin x ≈˘⟨ self x≈y ⟩ - f (f y) ≈⟨ inv y ⟩ + f (f y) ≈⟨ selfInverse⇒involutive y ⟩ y ∎ - selfInverse⇒bijective : Bijective f + selfInverse⇒bijective : Bijective _≈_ _≈_ f selfInverse⇒bijective = selfInverse⇒injective , selfInverse⇒surjective ------------------------------------------------------------------------ diff --git a/src/Algebra/Lattice/Morphism/Construct/Composition.agda b/src/Algebra/Lattice/Morphism/Construct/Composition.agda index 42f609c8de..fe5266af3d 100644 --- a/src/Algebra/Lattice/Morphism/Construct/Composition.agda +++ b/src/Algebra/Lattice/Morphism/Construct/Composition.agda @@ -57,5 +57,5 @@ module _ {L₁ : RawLattice a ℓ₁} → IsLatticeIsomorphism L₁ L₃ (g ∘ f) isLatticeIsomorphism f-iso g-iso = record { isLatticeMonomorphism = isLatticeMonomorphism F.isLatticeMonomorphism G.isLatticeMonomorphism - ; surjective = Func.surjective (_≈_ L₁) _ _ ≈₃-trans G.⟦⟧-cong F.surjective G.surjective + ; surjective = Func.surjective _ _ (_≈_ L₃) F.surjective G.surjective } where module F = IsLatticeIsomorphism f-iso; module G = IsLatticeIsomorphism g-iso diff --git a/src/Algebra/Lattice/Morphism/Construct/Identity.agda b/src/Algebra/Lattice/Morphism/Construct/Identity.agda index 9b5993696f..d69b53a899 100644 --- a/src/Algebra/Lattice/Morphism/Construct/Identity.agda +++ b/src/Algebra/Lattice/Morphism/Construct/Identity.agda @@ -13,6 +13,7 @@ open import Algebra.Lattice.Morphism.Structures using ( module LatticeMorphisms ) open import Data.Product using (_,_) open import Function.Base using (id) +import Function.Construct.Identity as Id open import Level using (Level) open import Relation.Binary.Morphism.Construct.Identity using (isRelHomomorphism) open import Relation.Binary.Definitions using (Reflexive) @@ -40,5 +41,5 @@ module _ (L : RawLattice c ℓ) (open RawLattice L) (refl : Reflexive _≈_) whe isLatticeIsomorphism : IsLatticeIsomorphism id isLatticeIsomorphism = record { isLatticeMonomorphism = isLatticeMonomorphism - ; surjective = _, refl + ; surjective = Id.surjective _ } diff --git a/src/Algebra/Lattice/Morphism/Structures.agda b/src/Algebra/Lattice/Morphism/Structures.agda index 7e7c34c163..87cf92e616 100644 --- a/src/Algebra/Lattice/Morphism/Structures.agda +++ b/src/Algebra/Lattice/Morphism/Structures.agda @@ -12,7 +12,7 @@ open import Algebra.Morphism open import Algebra.Lattice.Bundles import Algebra.Morphism.Definitions as MorphismDefinitions open import Level using (Level; _⊔_) -import Function.Definitions as FunctionDefinitions +open import Function.Definitions open import Relation.Binary.Morphism.Structures open import Relation.Binary.Core @@ -44,7 +44,6 @@ module LatticeMorphisms (L₁ : RawLattice a ℓ₁) (L₂ : RawLattice b ℓ₂ module ∧ = MagmaMorphisms ∧-rawMagma₁ ∧-rawMagma₂ open MorphismDefinitions A B _≈₂_ - open FunctionDefinitions _≈₁_ _≈₂_ record IsLatticeHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where @@ -71,7 +70,7 @@ module LatticeMorphisms (L₁ : RawLattice a ℓ₁) (L₂ : RawLattice b ℓ₂ record IsLatticeMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isLatticeHomomorphism : IsLatticeHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ + injective : Injective _≈₁_ _≈₂_ ⟦_⟧ open IsLatticeHomomorphism isLatticeHomomorphism public @@ -94,7 +93,7 @@ module LatticeMorphisms (L₁ : RawLattice a ℓ₁) (L₂ : RawLattice b ℓ₂ record IsLatticeIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isLatticeMonomorphism : IsLatticeMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ + surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧ open IsLatticeMonomorphism isLatticeMonomorphism public diff --git a/src/Algebra/Module/Morphism/Construct/Composition.agda b/src/Algebra/Module/Morphism/Construct/Composition.agda index 3aeb7a5f26..8c39496dd4 100644 --- a/src/Algebra/Module/Morphism/Construct/Composition.agda +++ b/src/Algebra/Module/Morphism/Construct/Composition.agda @@ -51,7 +51,7 @@ module _ IsLeftSemimoduleIsomorphism M₁ M₃ (g ∘ f) isLeftSemimoduleIsomorphism f-iso g-iso = record { isLeftSemimoduleMonomorphism = isLeftSemimoduleMonomorphism F.isLeftSemimoduleMonomorphism G.isLeftSemimoduleMonomorphism - ; surjective = Func.surjective (_≈ᴹ_ M₁) _ _ (≈ᴹ-trans M₃) G.⟦⟧-cong F.surjective G.surjective + ; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective } where module F = IsLeftSemimoduleIsomorphism f-iso; module G = IsLeftSemimoduleIsomorphism g-iso module _ @@ -85,7 +85,7 @@ module _ IsLeftModuleIsomorphism M₁ M₃ (g ∘ f) isLeftModuleIsomorphism f-iso g-iso = record { isLeftModuleMonomorphism = isLeftModuleMonomorphism F.isLeftModuleMonomorphism G.isLeftModuleMonomorphism - ; surjective = Func.surjective (_≈ᴹ_ M₁) _ _ (≈ᴹ-trans M₃) G.⟦⟧-cong F.surjective G.surjective + ; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective } where module F = IsLeftModuleIsomorphism f-iso; module G = IsLeftModuleIsomorphism g-iso module _ @@ -119,7 +119,7 @@ module _ IsRightSemimoduleIsomorphism M₁ M₃ (g ∘ f) isRightSemimoduleIsomorphism f-iso g-iso = record { isRightSemimoduleMonomorphism = isRightSemimoduleMonomorphism F.isRightSemimoduleMonomorphism G.isRightSemimoduleMonomorphism - ; surjective = Func.surjective (_≈ᴹ_ M₁) _ _ (≈ᴹ-trans M₃) G.⟦⟧-cong F.surjective G.surjective + ; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective } where module F = IsRightSemimoduleIsomorphism f-iso; module G = IsRightSemimoduleIsomorphism g-iso module _ @@ -153,7 +153,7 @@ module _ IsRightModuleIsomorphism M₁ M₃ (g ∘ f) isRightModuleIsomorphism f-iso g-iso = record { isRightModuleMonomorphism = isRightModuleMonomorphism F.isRightModuleMonomorphism G.isRightModuleMonomorphism - ; surjective = Func.surjective (_≈ᴹ_ M₁) _ _ (≈ᴹ-trans M₃) G.⟦⟧-cong F.surjective G.surjective + ; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective } where module F = IsRightModuleIsomorphism f-iso; module G = IsRightModuleIsomorphism g-iso module _ @@ -189,7 +189,7 @@ module _ IsBisemimoduleIsomorphism M₁ M₃ (g ∘ f) isBisemimoduleIsomorphism f-iso g-iso = record { isBisemimoduleMonomorphism = isBisemimoduleMonomorphism F.isBisemimoduleMonomorphism G.isBisemimoduleMonomorphism - ; surjective = Func.surjective (_≈ᴹ_ M₁) _ _ (≈ᴹ-trans M₃) G.⟦⟧-cong F.surjective G.surjective + ; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective } where module F = IsBisemimoduleIsomorphism f-iso; module G = IsBisemimoduleIsomorphism g-iso module _ @@ -225,7 +225,7 @@ module _ IsBimoduleIsomorphism M₁ M₃ (g ∘ f) isBimoduleIsomorphism f-iso g-iso = record { isBimoduleMonomorphism = isBimoduleMonomorphism F.isBimoduleMonomorphism G.isBimoduleMonomorphism - ; surjective = Func.surjective (_≈ᴹ_ M₁) _ _ (≈ᴹ-trans M₃) G.⟦⟧-cong F.surjective G.surjective + ; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective } where module F = IsBimoduleIsomorphism f-iso; module G = IsBimoduleIsomorphism g-iso module _ @@ -258,7 +258,7 @@ module _ IsSemimoduleIsomorphism M₁ M₃ (g ∘ f) isSemimoduleIsomorphism f-iso g-iso = record { isSemimoduleMonomorphism = isSemimoduleMonomorphism F.isSemimoduleMonomorphism G.isSemimoduleMonomorphism - ; surjective = Func.surjective (_≈ᴹ_ M₁) _ _ (≈ᴹ-trans M₃) G.⟦⟧-cong F.surjective G.surjective + ; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective } where module F = IsSemimoduleIsomorphism f-iso; module G = IsSemimoduleIsomorphism g-iso module _ @@ -291,5 +291,5 @@ module _ IsModuleIsomorphism M₁ M₃ (g ∘ f) isModuleIsomorphism f-iso g-iso = record { isModuleMonomorphism = isModuleMonomorphism F.isModuleMonomorphism G.isModuleMonomorphism - ; surjective = Func.surjective (_≈ᴹ_ M₁) _ _ (≈ᴹ-trans M₃) G.⟦⟧-cong F.surjective G.surjective + ; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective } where module F = IsModuleIsomorphism f-iso; module G = IsModuleIsomorphism g-iso diff --git a/src/Algebra/Module/Morphism/Construct/Identity.agda b/src/Algebra/Module/Morphism/Construct/Identity.agda index f5e5d73b05..7f56695dde 100644 --- a/src/Algebra/Module/Morphism/Construct/Identity.agda +++ b/src/Algebra/Module/Morphism/Construct/Identity.agda @@ -23,6 +23,7 @@ open import Algebra.Module.Morphism.Structures open import Algebra.Morphism.Construct.Identity open import Data.Product using (_,_) open import Function.Base using (id) +import Function.Construct.Identity as Id open import Level using (Level) private @@ -48,7 +49,7 @@ module _ {semiring : Semiring r ℓr} (M : LeftSemimodule semiring m ℓm) where isLeftSemimoduleIsomorphism : IsLeftSemimoduleIsomorphism id isLeftSemimoduleIsomorphism = record { isLeftSemimoduleMonomorphism = isLeftSemimoduleMonomorphism - ; surjective = _, ≈ᴹ-refl + ; surjective = Id.surjective _ } module _ {ring : Ring r ℓr} (M : LeftModule ring m ℓm) where @@ -70,7 +71,7 @@ module _ {ring : Ring r ℓr} (M : LeftModule ring m ℓm) where isLeftModuleIsomorphism : IsLeftModuleIsomorphism id isLeftModuleIsomorphism = record { isLeftModuleMonomorphism = isLeftModuleMonomorphism - ; surjective = _, ≈ᴹ-refl + ; surjective = Id.surjective _ } module _ {semiring : Semiring r ℓr} (M : RightSemimodule semiring m ℓm) where @@ -92,7 +93,7 @@ module _ {semiring : Semiring r ℓr} (M : RightSemimodule semiring m ℓm) wher isRightSemimoduleIsomorphism : IsRightSemimoduleIsomorphism id isRightSemimoduleIsomorphism = record { isRightSemimoduleMonomorphism = isRightSemimoduleMonomorphism - ; surjective = _, ≈ᴹ-refl + ; surjective = Id.surjective _ } module _ {ring : Ring r ℓr} (M : RightModule ring m ℓm) where @@ -114,7 +115,7 @@ module _ {ring : Ring r ℓr} (M : RightModule ring m ℓm) where isRightModuleIsomorphism : IsRightModuleIsomorphism id isRightModuleIsomorphism = record { isRightModuleMonomorphism = isRightModuleMonomorphism - ; surjective = _, ≈ᴹ-refl + ; surjective = Id.surjective _ } module _ {R-semiring : Semiring r ℓr} {S-semiring : Semiring s ℓs} (M : Bisemimodule R-semiring S-semiring m ℓm) where @@ -137,7 +138,7 @@ module _ {R-semiring : Semiring r ℓr} {S-semiring : Semiring s ℓs} (M : Bise isBisemimoduleIsomorphism : IsBisemimoduleIsomorphism id isBisemimoduleIsomorphism = record { isBisemimoduleMonomorphism = isBisemimoduleMonomorphism - ; surjective = _, ≈ᴹ-refl + ; surjective = Id.surjective _ } module _ {R-ring : Ring r ℓr} {S-ring : Ring r ℓr} (M : Bimodule R-ring S-ring m ℓm) where @@ -160,7 +161,7 @@ module _ {R-ring : Ring r ℓr} {S-ring : Ring r ℓr} (M : Bimodule R-ring S-ri isBimoduleIsomorphism : IsBimoduleIsomorphism id isBimoduleIsomorphism = record { isBimoduleMonomorphism = isBimoduleMonomorphism - ; surjective = _, ≈ᴹ-refl + ; surjective = Id.surjective _ } module _ {commutativeSemiring : CommutativeSemiring r ℓr} (M : Semimodule commutativeSemiring m ℓm) where @@ -181,7 +182,7 @@ module _ {commutativeSemiring : CommutativeSemiring r ℓr} (M : Semimodule comm isSemimoduleIsomorphism : IsSemimoduleIsomorphism id isSemimoduleIsomorphism = record { isSemimoduleMonomorphism = isSemimoduleMonomorphism - ; surjective = _, ≈ᴹ-refl + ; surjective = Id.surjective _ } module _ {commutativeRing : CommutativeRing r ℓr} (M : Module commutativeRing m ℓm) where @@ -202,5 +203,5 @@ module _ {commutativeRing : CommutativeRing r ℓr} (M : Module commutativeRing isModuleIsomorphism : IsModuleIsomorphism id isModuleIsomorphism = record { isModuleMonomorphism = isModuleMonomorphism - ; surjective = _, ≈ᴹ-refl + ; surjective = Id.surjective _ } diff --git a/src/Algebra/Module/Morphism/Structures.agda b/src/Algebra/Module/Morphism/Structures.agda index 3dc5fba3c5..96fb5ffa0a 100644 --- a/src/Algebra/Module/Morphism/Structures.agda +++ b/src/Algebra/Module/Morphism/Structures.agda @@ -11,7 +11,7 @@ open import Algebra.Bundles open import Algebra.Module.Bundles import Algebra.Module.Morphism.Definitions as MorphismDefinitions import Algebra.Morphism.Structures as MorphismStructures -import Function.Definitions as FunctionDefinitions +open import Function.Definitions open import Level private @@ -28,7 +28,6 @@ module LeftSemimoduleMorphisms open LeftSemimodule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _≈ᴹ_ to _≈ᴹ₁_) open LeftSemimodule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _≈ᴹ_ to _≈ᴹ₂_) open MorphismDefinitions R A B _≈ᴹ₂_ - open FunctionDefinitions _≈ᴹ₁_ _≈ᴹ₂_ open MorphismStructures.MonoidMorphisms (LeftSemimodule.+ᴹ-rawMonoid M₁) (LeftSemimodule.+ᴹ-rawMonoid M₂) record IsLeftSemimoduleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where @@ -43,7 +42,7 @@ module LeftSemimoduleMorphisms record IsLeftSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where field isLeftSemimoduleHomomorphism : IsLeftSemimoduleHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ + injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ open IsLeftSemimoduleHomomorphism isLeftSemimoduleHomomorphism public @@ -60,7 +59,7 @@ module LeftSemimoduleMorphisms record IsLeftSemimoduleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where field isLeftSemimoduleMonomorphism : IsLeftSemimoduleMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ + surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ open IsLeftSemimoduleMonomorphism isLeftSemimoduleMonomorphism public @@ -84,7 +83,6 @@ module LeftModuleMorphisms open LeftModule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _≈ᴹ_ to _≈ᴹ₁_) open LeftModule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _≈ᴹ_ to _≈ᴹ₂_) open MorphismDefinitions R A B _≈ᴹ₂_ - open FunctionDefinitions _≈ᴹ₁_ _≈ᴹ₂_ open MorphismStructures.GroupMorphisms (LeftModule.+ᴹ-rawGroup M₁) (LeftModule.+ᴹ-rawGroup M₂) open LeftSemimoduleMorphisms (LeftModule.leftSemimodule M₁) (LeftModule.leftSemimodule M₂) @@ -108,7 +106,7 @@ module LeftModuleMorphisms record IsLeftModuleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where field isLeftModuleHomomorphism : IsLeftModuleHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ + injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ open IsLeftModuleHomomorphism isLeftModuleHomomorphism public @@ -130,7 +128,7 @@ module LeftModuleMorphisms record IsLeftModuleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where field isLeftModuleMonomorphism : IsLeftModuleMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ + surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ open IsLeftModuleMonomorphism isLeftModuleMonomorphism public @@ -159,7 +157,6 @@ module RightSemimoduleMorphisms open RightSemimodule M₁ renaming (Carrierᴹ to A; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_) open RightSemimodule M₂ renaming (Carrierᴹ to B; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_) open MorphismDefinitions R A B _≈ᴹ₂_ - open FunctionDefinitions _≈ᴹ₁_ _≈ᴹ₂_ open MorphismStructures.MonoidMorphisms (RightSemimodule.+ᴹ-rawMonoid M₁) (RightSemimodule.+ᴹ-rawMonoid M₂) record IsRightSemimoduleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where @@ -174,7 +171,7 @@ module RightSemimoduleMorphisms record IsRightSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where field isRightSemimoduleHomomorphism : IsRightSemimoduleHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ + injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ open IsRightSemimoduleHomomorphism isRightSemimoduleHomomorphism public @@ -191,7 +188,7 @@ module RightSemimoduleMorphisms record IsRightSemimoduleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where field isRightSemimoduleMonomorphism : IsRightSemimoduleMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ + surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ open IsRightSemimoduleMonomorphism isRightSemimoduleMonomorphism public @@ -215,7 +212,6 @@ module RightModuleMorphisms open RightModule M₁ renaming (Carrierᴹ to A; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_) open RightModule M₂ renaming (Carrierᴹ to B; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_) open MorphismDefinitions R A B _≈ᴹ₂_ - open FunctionDefinitions _≈ᴹ₁_ _≈ᴹ₂_ open MorphismStructures.GroupMorphisms (RightModule.+ᴹ-rawGroup M₁) (RightModule.+ᴹ-rawGroup M₂) open RightSemimoduleMorphisms (RightModule.rightSemimodule M₁) (RightModule.rightSemimodule M₂) @@ -238,7 +234,7 @@ module RightModuleMorphisms record IsRightModuleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where field isRightModuleHomomorphism : IsRightModuleHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ + injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ open IsRightModuleHomomorphism isRightModuleHomomorphism public @@ -260,7 +256,7 @@ module RightModuleMorphisms record IsRightModuleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where field isRightModuleMonomorphism : IsRightModuleMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ + surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ open IsRightModuleMonomorphism isRightModuleMonomorphism public @@ -292,7 +288,6 @@ module BisemimoduleMorphisms open Bisemimodule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_) open MorphismDefinitions R A B _≈ᴹ₂_ using (Homomorphicₗ) open MorphismDefinitions S A B _≈ᴹ₂_ using (Homomorphicᵣ) - open FunctionDefinitions _≈ᴹ₁_ _≈ᴹ₂_ open MorphismStructures.MonoidMorphisms (Bisemimodule.+ᴹ-rawMonoid M₁) (Bisemimodule.+ᴹ-rawMonoid M₂) open LeftSemimoduleMorphisms (Bisemimodule.leftSemimodule M₁) (Bisemimodule.leftSemimodule M₂) open RightSemimoduleMorphisms (Bisemimodule.rightSemimodule M₁) (Bisemimodule.rightSemimodule M₂) @@ -321,7 +316,7 @@ module BisemimoduleMorphisms record IsBisemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ s ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where field isBisemimoduleHomomorphism : IsBisemimoduleHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ + injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ open IsBisemimoduleHomomorphism isBisemimoduleHomomorphism public @@ -343,7 +338,7 @@ module BisemimoduleMorphisms record IsBisemimoduleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ s ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where field isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ + surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ open IsBisemimoduleMonomorphism isBisemimoduleMonomorphism public @@ -375,7 +370,6 @@ module BimoduleMorphisms open Bimodule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_) open MorphismDefinitions R A B _≈ᴹ₂_ using (Homomorphicₗ) open MorphismDefinitions S A B _≈ᴹ₂_ using (Homomorphicᵣ) - open FunctionDefinitions _≈ᴹ₁_ _≈ᴹ₂_ open MorphismStructures.GroupMorphisms (Bimodule.+ᴹ-rawGroup M₁) (Bimodule.+ᴹ-rawGroup M₂) open LeftModuleMorphisms (Bimodule.leftModule M₁) (Bimodule.leftModule M₂) open RightModuleMorphisms (Bimodule.rightModule M₁) (Bimodule.rightModule M₂) @@ -418,7 +412,7 @@ module BimoduleMorphisms record IsBimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ s ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where field isBimoduleHomomorphism : IsBimoduleHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ + injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ open IsBimoduleHomomorphism isBimoduleHomomorphism public @@ -459,7 +453,7 @@ module BimoduleMorphisms record IsBimoduleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ s ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where field isBimoduleMonomorphism : IsBimoduleMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ + surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ open IsBimoduleMonomorphism isBimoduleMonomorphism public @@ -505,7 +499,6 @@ module SemimoduleMorphisms open Semimodule M₁ renaming (Carrierᴹ to A; _≈ᴹ_ to _≈ᴹ₁_) open Semimodule M₂ renaming (Carrierᴹ to B; _≈ᴹ_ to _≈ᴹ₂_) - open FunctionDefinitions _≈ᴹ₁_ _≈ᴹ₂_ open BisemimoduleMorphisms (Semimodule.bisemimodule M₁) (Semimodule.bisemimodule M₂) record IsSemimoduleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where @@ -517,7 +510,7 @@ module SemimoduleMorphisms record IsSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where field isSemimoduleHomomorphism : IsSemimoduleHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ + injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ open IsSemimoduleHomomorphism isSemimoduleHomomorphism public @@ -535,7 +528,7 @@ module SemimoduleMorphisms record IsSemimoduleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where field isSemimoduleMonomorphism : IsSemimoduleMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ + surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ open IsSemimoduleMonomorphism isSemimoduleMonomorphism public @@ -558,7 +551,6 @@ module ModuleMorphisms open Module M₁ renaming (Carrierᴹ to A; _≈ᴹ_ to _≈ᴹ₁_) open Module M₂ renaming (Carrierᴹ to B; _≈ᴹ_ to _≈ᴹ₂_) - open FunctionDefinitions _≈ᴹ₁_ _≈ᴹ₂_ open BimoduleMorphisms (Module.bimodule M₁) (Module.bimodule M₂) open SemimoduleMorphisms (Module.semimodule M₁) (Module.semimodule M₂) @@ -576,7 +568,7 @@ module ModuleMorphisms record IsModuleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where field isModuleHomomorphism : IsModuleHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ + injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ open IsModuleHomomorphism isModuleHomomorphism public @@ -601,7 +593,7 @@ module ModuleMorphisms record IsModuleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where field isModuleMonomorphism : IsModuleMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ + surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ open IsModuleMonomorphism isModuleMonomorphism public diff --git a/src/Algebra/Morphism/Consequences.agda b/src/Algebra/Morphism/Consequences.agda index d5bc6a8076..7f75506609 100644 --- a/src/Algebra/Morphism/Consequences.agda +++ b/src/Algebra/Morphism/Consequences.agda @@ -29,10 +29,10 @@ module _ {α α= β β=} (M₁ : Magma α α=) (M₂ : Magma β β=) where Inverseᵇ _≈₁_ _≈₂_ f g → Homomorphic₂ _ _ _≈₂_ f _∙₁_ _∙₂_ → Homomorphic₂ _ _ _≈₁_ g _∙₂_ _∙₁_ - homomorphic₂-inv {f} {g} g-cong (f∘g=id , g∘f=id) homo x y = begin - g (x ∙₂ y) ≈⟨ M₁.sym (g-cong (M₂.∙-cong (f∘g=id x) (f∘g=id y))) ⟩ - g (f (g x) ∙₂ f (g y)) ≈⟨ M₁.sym (g-cong (homo (g x) (g y))) ⟩ - g (f (g x ∙₁ g y)) ≈⟨ g∘f=id (g x ∙₁ g y) ⟩ + homomorphic₂-inv {f} {g} g-cong (invˡ , invʳ) homo x y = begin + g (x ∙₂ y) ≈˘⟨ g-cong (M₂.∙-cong (invˡ M₁.refl) (invˡ M₁.refl)) ⟩ + g (f (g x) ∙₂ f (g y)) ≈˘⟨ g-cong (homo (g x) (g y)) ⟩ + g (f (g x ∙₁ g y)) ≈⟨ invʳ M₂.refl ⟩ g x ∙₁ g y ∎ where open EqR M₁.setoid @@ -41,8 +41,8 @@ module _ {α α= β β=} (M₁ : Magma α α=) (M₂ : Magma β β=) where Homomorphic₂ _ _ _≈₂_ f _∙₁_ _∙₂_ → Homomorphic₂ _ _ _≈₁_ g _∙₂_ _∙₁_ homomorphic₂-inj {f} {g} inj invˡ homo x y = inj (begin - f (g (x ∙₂ y)) ≈⟨ invˡ (x ∙₂ y) ⟩ - x ∙₂ y ≈⟨ M₂.sym (M₂.∙-cong (invˡ x) (invˡ y)) ⟩ - f (g x) ∙₂ f (g y) ≈⟨ M₂.sym (homo (g x) (g y)) ⟩ + f (g (x ∙₂ y)) ≈⟨ invˡ M₁.refl ⟩ + x ∙₂ y ≈˘⟨ M₂.∙-cong (invˡ M₁.refl) (invˡ M₁.refl) ⟩ + f (g x) ∙₂ f (g y) ≈˘⟨ homo (g x) (g y) ⟩ f (g x ∙₁ g y) ∎) where open EqR M₂.setoid diff --git a/src/Algebra/Morphism/Construct/Composition.agda b/src/Algebra/Morphism/Construct/Composition.agda index 991fb93433..e3f3a3ad71 100644 --- a/src/Algebra/Morphism/Construct/Composition.agda +++ b/src/Algebra/Morphism/Construct/Composition.agda @@ -57,7 +57,7 @@ module _ {M₁ : RawMagma a ℓ₁} → IsMagmaIsomorphism M₁ M₃ (g ∘ f) isMagmaIsomorphism f-iso g-iso = record { isMagmaMonomorphism = isMagmaMonomorphism F.isMagmaMonomorphism G.isMagmaMonomorphism - ; surjective = Func.surjective (_≈_ M₁) _ _ ≈₃-trans G.⟦⟧-cong F.surjective G.surjective + ; surjective = Func.surjective _ _ (_≈_ M₃) F.surjective G.surjective } where module F = IsMagmaIsomorphism f-iso; module G = IsMagmaIsomorphism g-iso @@ -97,7 +97,7 @@ module _ {M₁ : RawMonoid a ℓ₁} → IsMonoidIsomorphism M₁ M₃ (g ∘ f) isMonoidIsomorphism f-iso g-iso = record { isMonoidMonomorphism = isMonoidMonomorphism F.isMonoidMonomorphism G.isMonoidMonomorphism - ; surjective = Func.surjective (_≈_ M₁) _ _ ≈₃-trans G.⟦⟧-cong F.surjective G.surjective + ; surjective = Func.surjective _ _(_≈_ M₃) F.surjective G.surjective } where module F = IsMonoidIsomorphism f-iso; module G = IsMonoidIsomorphism g-iso @@ -138,7 +138,7 @@ module _ {G₁ : RawGroup a ℓ₁} → IsGroupIsomorphism G₁ G₃ (g ∘ f) isGroupIsomorphism f-iso g-iso = record { isGroupMonomorphism = isGroupMonomorphism F.isGroupMonomorphism G.isGroupMonomorphism - ; surjective = Func.surjective (_≈_ G₁) _ _ ≈₃-trans G.⟦⟧-cong F.surjective G.surjective + ; surjective = Func.surjective _ _ (_≈_ G₃) F.surjective G.surjective } where module F = IsGroupIsomorphism f-iso; module G = IsGroupIsomorphism g-iso @@ -178,7 +178,7 @@ module _ {R₁ : RawNearSemiring a ℓ₁} → IsNearSemiringIsomorphism R₁ R₃ (g ∘ f) isNearSemiringIsomorphism f-iso g-iso = record { isNearSemiringMonomorphism = isNearSemiringMonomorphism F.isNearSemiringMonomorphism G.isNearSemiringMonomorphism - ; surjective = Func.surjective (_≈_ R₁) _ _ ≈₃-trans G.⟦⟧-cong F.surjective G.surjective + ; surjective = Func.surjective _ _ (_≈_ R₃) F.surjective G.surjective } where module F = IsNearSemiringIsomorphism f-iso; module G = IsNearSemiringIsomorphism g-iso @@ -220,7 +220,7 @@ module _ → IsSemiringIsomorphism R₁ R₃ (g ∘ f) isSemiringIsomorphism f-iso g-iso = record { isSemiringMonomorphism = isSemiringMonomorphism F.isSemiringMonomorphism G.isSemiringMonomorphism - ; surjective = Func.surjective (_≈_ R₁) _ _ ≈₃-trans G.⟦⟧-cong F.surjective G.surjective + ; surjective = Func.surjective _ _ (_≈_ R₃) F.surjective G.surjective } where module F = IsSemiringIsomorphism f-iso; module G = IsSemiringIsomorphism g-iso ------------------------------------------------------------------------ @@ -260,7 +260,7 @@ module _ {R₁ : RawRingWithoutOne a ℓ₁} → IsRingWithoutOneIsoMorphism R₁ R₃ (g ∘ f) isRingWithoutOneIsoMorphism f-iso g-iso = record { isRingWithoutOneMonomorphism = isRingWithoutOneMonomorphism F.isRingWithoutOneMonomorphism G.isRingWithoutOneMonomorphism - ; surjective = Func.surjective (_≈_ R₁) (_≈_ R₂) (_≈_ R₃) ≈₃-trans G.⟦⟧-cong F.surjective G.surjective + ; surjective = Func.surjective _ _ (_≈_ R₃) F.surjective G.surjective } where module F = IsRingWithoutOneIsoMorphism f-iso; module G = IsRingWithoutOneIsoMorphism g-iso ------------------------------------------------------------------------ @@ -300,7 +300,7 @@ module _ {R₁ : RawRing a ℓ₁} → IsRingIsomorphism R₁ R₃ (g ∘ f) isRingIsomorphism f-iso g-iso = record { isRingMonomorphism = isRingMonomorphism F.isRingMonomorphism G.isRingMonomorphism - ; surjective = Func.surjective (_≈_ R₁) _ _ ≈₃-trans G.⟦⟧-cong F.surjective G.surjective + ; surjective = Func.surjective _ _ (_≈_ R₃) F.surjective G.surjective } where module F = IsRingIsomorphism f-iso; module G = IsRingIsomorphism g-iso ------------------------------------------------------------------------ @@ -342,7 +342,7 @@ module _ {Q₁ : RawQuasigroup a ℓ₁} → IsQuasigroupIsomorphism Q₁ Q₃ (g ∘ f) isQuasigroupIsomorphism f-iso g-iso = record { isQuasigroupMonomorphism = isQuasigroupMonomorphism F.isQuasigroupMonomorphism G.isQuasigroupMonomorphism - ; surjective = Func.surjective (_≈_ Q₁) (_≈_ Q₂) (_≈_ Q₃) ≈₃-trans G.⟦⟧-cong F.surjective G.surjective + ; surjective = Func.surjective _ _ (_≈_ Q₃) F.surjective G.surjective } where module F = IsQuasigroupIsomorphism f-iso; module G = IsQuasigroupIsomorphism g-iso ------------------------------------------------------------------------ @@ -382,5 +382,5 @@ module _ {L₁ : RawLoop a ℓ₁} → IsLoopIsomorphism L₁ L₃ (g ∘ f) isLoopIsomorphism f-iso g-iso = record { isLoopMonomorphism = isLoopMonomorphism F.isLoopMonomorphism G.isLoopMonomorphism - ; surjective = Func.surjective (_≈_ L₁) (_≈_ L₂) (_≈_ L₃) ≈₃-trans G.⟦⟧-cong F.surjective G.surjective + ; surjective = Func.surjective _ _ (_≈_ L₃) F.surjective G.surjective } where module F = IsLoopIsomorphism f-iso; module G = IsLoopIsomorphism g-iso diff --git a/src/Algebra/Morphism/Construct/Identity.agda b/src/Algebra/Morphism/Construct/Identity.agda index 5ea2571de0..c1b161380b 100644 --- a/src/Algebra/Morphism/Construct/Identity.agda +++ b/src/Algebra/Morphism/Construct/Identity.agda @@ -22,6 +22,7 @@ open import Algebra.Morphism.Structures ) open import Data.Product using (_,_) open import Function.Base using (id) +import Function.Construct.Identity as Id open import Level using (Level) open import Relation.Binary.Morphism.Construct.Identity using (isRelHomomorphism) open import Relation.Binary.Definitions using (Reflexive) @@ -51,7 +52,7 @@ module _ (M : RawMagma c ℓ) (open RawMagma M) (refl : Reflexive _≈_) where isMagmaIsomorphism : IsMagmaIsomorphism id isMagmaIsomorphism = record { isMagmaMonomorphism = isMagmaMonomorphism - ; surjective = _, refl + ; surjective = Id.surjective _ } ------------------------------------------------------------------------ @@ -75,7 +76,7 @@ module _ (M : RawMonoid c ℓ) (open RawMonoid M) (refl : Reflexive _≈_) where isMonoidIsomorphism : IsMonoidIsomorphism id isMonoidIsomorphism = record { isMonoidMonomorphism = isMonoidMonomorphism - ; surjective = _, refl + ; surjective = Id.surjective _ } ------------------------------------------------------------------------ @@ -99,7 +100,7 @@ module _ (G : RawGroup c ℓ) (open RawGroup G) (refl : Reflexive _≈_) where isGroupIsomorphism : IsGroupIsomorphism id isGroupIsomorphism = record { isGroupMonomorphism = isGroupMonomorphism - ; surjective = _, refl + ; surjective = Id.surjective _ } ------------------------------------------------------------------------ @@ -123,7 +124,7 @@ module _ (R : RawNearSemiring c ℓ) (open RawNearSemiring R) (refl : Reflexive isNearSemiringIsomorphism : IsNearSemiringIsomorphism id isNearSemiringIsomorphism = record { isNearSemiringMonomorphism = isNearSemiringMonomorphism - ; surjective = _, refl + ; surjective = Id.surjective _ } ------------------------------------------------------------------------ @@ -147,7 +148,7 @@ module _ (R : RawSemiring c ℓ) (open RawSemiring R) (refl : Reflexive _≈_) w isSemiringIsomorphism : IsSemiringIsomorphism id isSemiringIsomorphism = record { isSemiringMonomorphism = isSemiringMonomorphism - ; surjective = _, refl + ; surjective = Id.surjective _ } ------------------------------------------------------------------------ @@ -171,7 +172,7 @@ module _ (R : RawRingWithoutOne c ℓ) (open RawRingWithoutOne R) (refl : Reflex isRingWithoutOneIsoMorphism : IsRingWithoutOneIsoMorphism id isRingWithoutOneIsoMorphism = record { isRingWithoutOneMonomorphism = isRingWithoutOneMonomorphism - ; surjective = _, refl + ; surjective = Id.surjective _ } ------------------------------------------------------------------------ @@ -195,7 +196,7 @@ module _ (R : RawRing c ℓ) (open RawRing R) (refl : Reflexive _≈_) where isRingIsomorphism : IsRingIsomorphism id isRingIsomorphism = record { isRingMonomorphism = isRingMonomorphism - ; surjective = _, refl + ; surjective = Id.surjective _ } ------------------------------------------------------------------------ @@ -221,7 +222,7 @@ module _ (Q : RawQuasigroup c ℓ) (open RawQuasigroup Q) (refl : Reflexive _≈ isQuasigroupIsomorphism : IsQuasigroupIsomorphism id isQuasigroupIsomorphism = record { isQuasigroupMonomorphism = isQuasigroupMonomorphism - ; surjective = _, refl + ; surjective = Id.surjective _ } ------------------------------------------------------------------------ @@ -245,5 +246,5 @@ module _ (L : RawLoop c ℓ) (open RawLoop L) (refl : Reflexive _≈_) where isLoopIsomorphism : IsLoopIsomorphism id isLoopIsomorphism = record { isLoopMonomorphism = isLoopMonomorphism - ; surjective = _, refl + ; surjective = Id.surjective _ } diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda index 525cbf5da0..eb8970ba5c 100644 --- a/src/Algebra/Morphism/Structures.agda +++ b/src/Algebra/Morphism/Structures.agda @@ -14,7 +14,7 @@ open import Algebra.Core open import Algebra.Bundles import Algebra.Morphism.Definitions as MorphismDefinitions open import Level using (Level; _⊔_) -import Function.Definitions as FunctionDefinitions +open import Function.Definitions open import Relation.Binary.Morphism.Structures private @@ -30,7 +30,6 @@ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) wher open RawMagma M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_) open RawMagma M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_) open MorphismDefinitions A B _≈₂_ - open FunctionDefinitions _≈₁_ _≈₂_ record IsMagmaHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where @@ -45,7 +44,7 @@ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) wher record IsMagmaMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isMagmaHomomorphism : IsMagmaHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ + injective : Injective _≈₁_ _≈₂_ ⟦_⟧ open IsMagmaHomomorphism isMagmaHomomorphism public @@ -59,7 +58,7 @@ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) wher record IsMagmaIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isMagmaMonomorphism : IsMagmaMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ + surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧ open IsMagmaMonomorphism isMagmaMonomorphism public @@ -79,7 +78,6 @@ module MonoidMorphisms (M₁ : RawMonoid a ℓ₁) (M₂ : RawMonoid b ℓ₂) w open RawMonoid M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; ε to ε₁) open RawMonoid M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; ε to ε₂) open MorphismDefinitions A B _≈₂_ - open FunctionDefinitions _≈₁_ _≈₂_ open MagmaMorphisms (RawMonoid.rawMagma M₁) (RawMonoid.rawMagma M₂) @@ -94,7 +92,7 @@ module MonoidMorphisms (M₁ : RawMonoid a ℓ₁) (M₂ : RawMonoid b ℓ₂) w record IsMonoidMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ + injective : Injective _≈₁_ _≈₂_ ⟦_⟧ open IsMonoidHomomorphism isMonoidHomomorphism public @@ -111,7 +109,7 @@ module MonoidMorphisms (M₁ : RawMonoid a ℓ₁) (M₂ : RawMonoid b ℓ₂) w record IsMonoidIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isMonoidMonomorphism : IsMonoidMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ + surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧ open IsMonoidMonomorphism isMonoidMonomorphism public @@ -136,7 +134,6 @@ module GroupMorphisms (G₁ : RawGroup a ℓ₁) (G₂ : RawGroup b ℓ₂) wher open RawGroup G₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; _⁻¹ to _⁻¹₂; ε to ε₂) open MorphismDefinitions A B _≈₂_ - open FunctionDefinitions _≈₁_ _≈₂_ open MagmaMorphisms (RawGroup.rawMagma G₁) (RawGroup.rawMagma G₂) open MonoidMorphisms (RawGroup.rawMonoid G₁) (RawGroup.rawMonoid G₂) @@ -152,7 +149,7 @@ module GroupMorphisms (G₁ : RawGroup a ℓ₁) (G₂ : RawGroup b ℓ₂) wher record IsGroupMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isGroupHomomorphism : IsGroupHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ + injective : Injective _≈₁_ _≈₂_ ⟦_⟧ open IsGroupHomomorphism isGroupHomomorphism public renaming (homo to ∙-homo) @@ -170,7 +167,7 @@ module GroupMorphisms (G₁ : RawGroup a ℓ₁) (G₂ : RawGroup b ℓ₂) wher record IsGroupIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isGroupMonomorphism : IsGroupMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ + surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧ open IsGroupMonomorphism isGroupMonomorphism public @@ -207,7 +204,6 @@ module NearSemiringMorphisms (R₁ : RawNearSemiring a ℓ₁) (R₂ : RawNearSe module * = MagmaMorphisms *-rawMagma₁ *-rawMagma₂ open MorphismDefinitions A B _≈₂_ - open FunctionDefinitions _≈₁_ _≈₂_ record IsNearSemiringHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where @@ -227,7 +223,7 @@ module NearSemiringMorphisms (R₁ : RawNearSemiring a ℓ₁) (R₂ : RawNearSe record IsNearSemiringMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ + injective : Injective _≈₁_ _≈₂_ ⟦_⟧ open IsNearSemiringHomomorphism isNearSemiringHomomorphism public @@ -250,7 +246,7 @@ module NearSemiringMorphisms (R₁ : RawNearSemiring a ℓ₁) (R₂ : RawNearSe record IsNearSemiringIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isNearSemiringMonomorphism : IsNearSemiringMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ + surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧ open IsNearSemiringMonomorphism isNearSemiringMonomorphism public @@ -292,7 +288,6 @@ module SemiringMorphisms (R₁ : RawSemiring a ℓ₁) (R₂ : RawSemiring b ℓ module * = MonoidMorphisms *-rawMonoid₁ *-rawMonoid₂ open MorphismDefinitions A B _≈₂_ - open FunctionDefinitions _≈₁_ _≈₂_ open NearSemiringMorphisms rawNearSemiring₁ rawNearSemiring₂ record IsSemiringHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where @@ -311,7 +306,7 @@ module SemiringMorphisms (R₁ : RawSemiring a ℓ₁) (R₂ : RawSemiring b ℓ record IsSemiringMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isSemiringHomomorphism : IsSemiringHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ + injective : Injective _≈₁_ _≈₂_ ⟦_⟧ open IsSemiringHomomorphism isSemiringHomomorphism public @@ -333,7 +328,7 @@ module SemiringMorphisms (R₁ : RawSemiring a ℓ₁) (R₂ : RawSemiring b ℓ record IsSemiringIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isSemiringMonomorphism : IsSemiringMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ + surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧ open IsSemiringMonomorphism isSemiringMonomorphism public @@ -375,7 +370,6 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi module * = MagmaMorphisms *-rawMagma₁ *-rawMagma₂ open MorphismDefinitions A B _≈₂_ - open FunctionDefinitions _≈₁_ _≈₂_ record IsRingWithoutOneHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field @@ -394,7 +388,7 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi record IsRingWithoutOneMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ + injective : Injective _≈₁_ _≈₂_ ⟦_⟧ open IsRingWithoutOneHomomorphism isRingWithoutOneHomomorphism public @@ -417,7 +411,7 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi record IsRingWithoutOneIsoMorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isRingWithoutOneMonomorphism : IsRingWithoutOneMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ + surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧ open IsRingWithoutOneMonomorphism isRingWithoutOneMonomorphism public @@ -462,7 +456,6 @@ module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where module * = MonoidMorphisms *-rawMonoid₁ *-rawMonoid₂ open MorphismDefinitions A B _≈₂_ - open FunctionDefinitions _≈₁_ _≈₂_ open SemiringMorphisms rawSemiring₁ rawSemiring₂ @@ -482,7 +475,7 @@ module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where record IsRingMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isRingHomomorphism : IsRingHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ + injective : Injective _≈₁_ _≈₂_ ⟦_⟧ open IsRingHomomorphism isRingHomomorphism public @@ -518,7 +511,7 @@ module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where record IsRingIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isRingMonomorphism : IsRingMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ + surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧ open IsRingMonomorphism isRingMonomorphism public @@ -568,7 +561,6 @@ module QuasigroupMorphisms (Q₁ : RawQuasigroup a ℓ₁) (Q₂ : RawQuasigroup module // = MagmaMorphisms //-rawMagma₁ //-rawMagma₂ open MorphismDefinitions A B _≈₂_ - open FunctionDefinitions _≈₁_ _≈₂_ record IsQuasigroupHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field @@ -601,7 +593,7 @@ module QuasigroupMorphisms (Q₁ : RawQuasigroup a ℓ₁) (Q₂ : RawQuasigroup record IsQuasigroupMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isQuasigroupHomomorphism : IsQuasigroupHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ + injective : Injective _≈₁_ _≈₂_ ⟦_⟧ open IsQuasigroupHomomorphism isQuasigroupHomomorphism public @@ -631,7 +623,7 @@ module QuasigroupMorphisms (Q₁ : RawQuasigroup a ℓ₁) (Q₂ : RawQuasigroup record IsQuasigroupIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isQuasigroupMonomorphism : IsQuasigroupMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ + surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧ open IsQuasigroupMonomorphism isQuasigroupMonomorphism public @@ -669,7 +661,6 @@ module LoopMorphisms (L₁ : RawLoop a ℓ₁) (L₂ : RawLoop b ℓ₂) where \\-rawMagma to \\-rawMagma₂; //-rawMagma to //-rawMagma₂; _≈_ to _≈₂_; _∙_ to _∙₂_; _\\_ to _\\₂_; _//_ to _//₂_ ; ε to ε₂) open MorphismDefinitions A B _≈₂_ - open FunctionDefinitions _≈₁_ _≈₂_ open QuasigroupMorphisms (RawLoop.rawQuasigroup L₁) (RawLoop.rawQuasigroup L₂) @@ -683,14 +674,14 @@ module LoopMorphisms (L₁ : RawLoop a ℓ₁) (L₂ : RawLoop b ℓ₂) where record IsLoopMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isLoopHomomorphism : IsLoopHomomorphism ⟦_⟧ - injective : Injective ⟦_⟧ + injective : Injective _≈₁_ _≈₂_ ⟦_⟧ open IsLoopHomomorphism isLoopHomomorphism public record IsLoopIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isLoopMonomorphism : IsLoopMonomorphism ⟦_⟧ - surjective : Surjective ⟦_⟧ + surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧ open IsLoopMonomorphism isLoopMonomorphism public diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda index f6a7820b52..26a175a0d5 100644 --- a/src/Data/Fin/Permutation.agda +++ b/src/Data/Fin/Permutation.agda @@ -20,7 +20,7 @@ open import Function.Bundles using (_↔_; Injection; Inverse; mk↔′) open import Function.Construct.Composition using (_↔-∘_) open import Function.Construct.Identity using (↔-id) open import Function.Construct.Symmetry using (↔-sym) -open import Function.Definitions using (Inverseˡ; Inverseʳ) +open import Function.Definitions open import Function.Equality using (_⟨$⟩_) open import Function.Properties.Inverse using (↔⇒↣) open import Function.Base using (_∘_) @@ -57,7 +57,7 @@ Permutation′ n = Permutation n n -- Helper functions permutation : ∀ (f : Fin m → Fin n) (g : Fin n → Fin m) → - Inverseˡ _≡_ _≡_ f g → Inverseʳ _≡_ _≡_ f g → Permutation m n + StrictlyInverseˡ _≡_ f g → StrictlyInverseʳ _≡_ f g → Permutation m n permutation = mk↔′ infixl 5 _⟨$⟩ʳ_ _⟨$⟩ˡ_ @@ -68,10 +68,10 @@ _⟨$⟩ˡ_ : Permutation m n → Fin n → Fin m _⟨$⟩ˡ_ = Inverse.from inverseˡ : ∀ (π : Permutation m n) {i} → π ⟨$⟩ˡ (π ⟨$⟩ʳ i) ≡ i -inverseˡ π = Inverse.inverseʳ π _ +inverseˡ π = Inverse.inverseʳ π P.refl inverseʳ : ∀ (π : Permutation m n) {i} → π ⟨$⟩ʳ (π ⟨$⟩ˡ i) ≡ i -inverseʳ π = Inverse.inverseˡ π _ +inverseʳ π = Inverse.inverseˡ π P.refl ------------------------------------------------------------------------ -- Equality @@ -142,7 +142,7 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′ from : Fin n → Fin m from j = punchOut {j = πˡ (punchIn (πʳ i) j)} from-punchOut - inverseʳ′ : Inverseʳ _≡_ _≡_ to from + inverseʳ′ : StrictlyInverseʳ _≡_ to from inverseʳ′ j = begin from (to j) ≡⟨⟩ punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _ ≡⟨ punchOut-cong′ i (cong πˡ (punchIn-punchOut _)) ⟩ @@ -150,7 +150,7 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′ punchOut {i = i} {punchIn i j} _ ≡⟨ punchOut-punchIn i ⟩ j ∎ - inverseˡ′ : Inverseˡ _≡_ _≡_ to from + inverseˡ′ : StrictlyInverseˡ _≡_ to from inverseˡ′ j = begin to (from j) ≡⟨⟩ punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))} _ ≡⟨ punchOut-cong′ (πʳ i) (cong πʳ (punchIn-punchOut _)) ⟩ @@ -171,11 +171,11 @@ lift₀ {m} {n} π = permutation to from inverseˡ′ inverseʳ′ from 0F = 0F from (suc i) = suc (π ⟨$⟩ˡ i) - inverseʳ′ : Inverseʳ _≡_ _≡_ to from + inverseʳ′ : StrictlyInverseʳ _≡_ to from inverseʳ′ 0F = refl inverseʳ′ (suc j) = cong suc (inverseˡ π) - inverseˡ′ : Inverseˡ _≡_ _≡_ to from + inverseˡ′ : StrictlyInverseˡ _≡_ to from inverseˡ′ 0F = refl inverseˡ′ (suc j) = cong suc (inverseʳ π) @@ -194,7 +194,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′ ... | yes j≡k = i ... | no j≢k = punchIn i (π ⟨$⟩ˡ punchOut j≢k) - inverseʳ′ : Inverseʳ _≡_ _≡_ to from + inverseʳ′ : StrictlyInverseʳ _≡_ to from inverseʳ′ k with i ≟ k ... | yes i≡k rewrite proj₂ (dec-yes (j ≟ j) refl) = i≡k ... | no i≢k @@ -207,7 +207,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′ punchIn i (punchOut i≢k) ≡⟨ punchIn-punchOut i≢k ⟩ k ∎ - inverseˡ′ : Inverseˡ _≡_ _≡_ to from + inverseˡ′ : StrictlyInverseˡ _≡_ to from inverseˡ′ k with j ≟ k ... | yes j≡k rewrite proj₂ (dec-yes (i ≟ i) refl) = j≡k ... | no j≢k diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index d7a963f9fd..b5df5aefdf 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -29,9 +29,8 @@ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′) open import Data.Sum.Properties using ([,]-map; [,]-∘) open import Function.Base using (_∘_; id; _$_; flip) open import Function.Bundles using (Injection; _↣_; _⇔_; _↔_; mk⇔; mk↔′) -open import Function.Definitions using (Injective) -open import Function.Definitions.Core2 using (Surjective) -open import Function.Consequences using (contraInjective) +open import Function.Definitions using (Injective; Surjective) +open import Function.Consequences.Propositional using (contraInjective) open import Function.Construct.Composition as Comp hiding (injective) open import Level using (Level) open import Relation.Binary as B hiding (Decidable; _⇔_) @@ -867,10 +866,10 @@ punchOut-punchIn (suc i) {suc j} = cong suc (begin -- pinch ------------------------------------------------------------------------ -pinch-surjective : ∀ (i : Fin n) → Surjective _≡_ (pinch i) -pinch-surjective _ zero = zero , refl -pinch-surjective zero (suc j) = suc (suc j) , refl -pinch-surjective (suc i) (suc j) = map suc (cong suc) (pinch-surjective i j) +pinch-surjective : ∀ (i : Fin n) → Surjective _≡_ _≡_ (pinch i) +pinch-surjective _ zero = zero , λ { refl → refl } +pinch-surjective zero (suc j) = suc (suc j) , λ { refl → refl } +pinch-surjective (suc i) (suc j) = map suc (λ {f refl → cong suc (f refl)}) (pinch-surjective i j) pinch-mono-≤ : ∀ (i : Fin n) → (pinch i) Preserves _≤_ ⟶ _≤_ pinch-mono-≤ 0F {0F} {k} 0≤n = z≤n @@ -987,8 +986,8 @@ injective⇒≤ {zero} {_} {f} _ = z≤n injective⇒≤ {suc _} {zero} {f} _ = contradiction (f zero) ¬Fin0 injective⇒≤ {suc _} {suc _} {f} inj = s≤s (injective⇒≤ (λ eq → suc-injective (inj (punchOut-injective - (contraInjective _≡_ _≡_ inj 0≢1+n) - (contraInjective _≡_ _≡_ inj 0≢1+n) eq)))) + (contraInjective inj 0≢1+n) + (contraInjective inj 0≢1+n) eq)))) <⇒notInjective : ∀ {f : Fin m → Fin n} → n ℕ.< m → ¬ (Injective _≡_ _≡_ f) <⇒notInjective n; proj₂; uncurry) open import Function.Base open import Function.Bundles using (_⤖_; _⇔_ ; mk⤖; mk⇔) - +open import Function.Consequences.Propositional using (strictlySurjective⇒surjective) open import Relation.Nullary.Reflects using (invert) open import Relation.Nullary using (Dec; does; _because_; yes; no; ¬_) open import Relation.Nullary.Decidable as Dec using (¬?) @@ -345,7 +345,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where toAny∘fromAny≗id (there p) = P.cong there (toAny∘fromAny≗id p) Sublist-[x]-bijection : ∀ {x xs} → (Sublist R [ x ] xs) ⤖ (Any (R x) xs) - Sublist-[x]-bijection = mk⤖ (toAny-injective , < fromAny , toAny∘fromAny≗id >) + Sublist-[x]-bijection = mk⤖ (toAny-injective , strictlySurjective⇒surjective < fromAny , toAny∘fromAny≗id >) ------------------------------------------------------------------------ -- Relational properties diff --git a/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda b/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda index b9eabc66b3..7b0eea3733 100644 --- a/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda +++ b/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda @@ -18,14 +18,14 @@ open import Data.Product using (_,_; proj₁; proj₂) open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) open import Function +open import Function.Consequences open import Level open import Relation.Binary -open import Relation.Binary.PropositionalEquality using (_≡_) +open import Relation.Binary.PropositionalEquality as P using (_≡_) open import Relation.Binary.Properties.Setoid using (respʳ-flip) module Data.List.Relation.Unary.Enumerates.Setoid.Properties where -open Setoid private variable @@ -38,7 +38,7 @@ module _ (S : Setoid a ℓ₁) (T : Setoid b ℓ₂) (surj : Surjection S T) whe open Surjection surj map⁺ : ∀ {xs} → IsEnumeration S xs → IsEnumeration T (map to xs) - map⁺ _∈xs y with surjective y + map⁺ _∈xs y with strictlySurjective y ... | (x , fx≈y) = ∈-resp-≈ T fx≈y (∈-map⁺ S T cong (x ∈xs)) ------------------------------------------------------------------------ @@ -82,7 +82,9 @@ module _ (S? : DecSetoid a ℓ₁) where -- lookup module _ (S : Setoid a ℓ₁) where + open Setoid S lookup-surjective : ∀ {xs} → IsEnumeration S xs → - Surjective _≡_ (_≈_ S) (lookup xs) - lookup-surjective _∈xs y = index (y ∈xs) , sym S (lookup-index (y ∈xs)) + Surjective _≡_ _≈_ (lookup xs) + lookup-surjective _∈xs = strictlySurjective⇒surjective + trans (λ { P.refl → refl}) (λ y → index (y ∈xs) , sym (lookup-index (y ∈xs))) diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index 3ea094ec00..b02dc90897 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -24,8 +24,8 @@ open import Data.Nat.Solver open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Function.Base using (_∘_; _$_; id) -open import Function.Definitions using (Injective) -open import Function.Definitions.Core2 using (Surjective) +open import Function.Definitions +open import Function.Consequences.Propositional open import Level using (0ℓ) open import Relation.Binary open import Relation.Binary.Consequences @@ -196,8 +196,8 @@ toℕ-injective {1+[2 x ]} {1+[2 y ]} 1+2xN≡1+2yN = cong 1+[2_] x≡y xN≡yN = ℕₚ.*-cancelˡ-≡ _ _ 2 2xN≡2yN x≡y = toℕ-injective xN≡yN -toℕ-surjective : Surjective _≡_ toℕ -toℕ-surjective n = (fromℕ n , toℕ-fromℕ n) +toℕ-surjective : Surjective _≡_ _≡_ toℕ +toℕ-surjective = strictlySurjective⇒surjective (λ n → fromℕ n , toℕ-fromℕ n) toℕ-isRelHomomorphism : IsRelHomomorphism _≡_ _≡_ toℕ toℕ-isRelHomomorphism = record @@ -215,6 +215,15 @@ fromℕ-injective {x} {y} f[x]≡f[y] = begin fromℕ-toℕ : fromℕ ∘ toℕ ≗ id fromℕ-toℕ = toℕ-injective ∘ toℕ-fromℕ ∘ toℕ +toℕ-inverseˡ : Inverseˡ _≡_ _≡_ toℕ fromℕ +toℕ-inverseˡ = strictlyInverseˡ⇒inverseˡ {f⁻¹ = fromℕ} toℕ toℕ-fromℕ + +toℕ-inverseʳ : Inverseʳ _≡_ _≡_ toℕ fromℕ +toℕ-inverseʳ = strictlyInverseʳ⇒inverseʳ toℕ fromℕ-toℕ + +toℕ-inverseᵇ : Inverseᵇ _≡_ _≡_ toℕ fromℕ +toℕ-inverseᵇ = toℕ-inverseˡ , toℕ-inverseʳ + fromℕ-pred : ∀ n → fromℕ (ℕ.pred n) ≡ pred (fromℕ n) fromℕ-pred n = begin fromℕ (ℕ.pred n) ≡⟨ cong (fromℕ ∘ ℕ.pred) (sym (toℕ-fromℕ n)) ⟩ diff --git a/src/Data/Nat/Binary/Subtraction.agda b/src/Data/Nat/Binary/Subtraction.agda index 67eebc88f6..46246707f4 100644 --- a/src/Data/Nat/Binary/Subtraction.agda +++ b/src/Data/Nat/Binary/Subtraction.agda @@ -109,8 +109,8 @@ toℕ-homo-∸ 1+[2 x ] 1+[2 y ] = begin where open ≡-Reasoning fromℕ-homo-∸ : ∀ m n → fromℕ (m ℕ.∸ n) ≡ (fromℕ m) ∸ (fromℕ n) -fromℕ-homo-∸ = homomorphic₂-inv ∸-magma ℕₚ.∸-magma {toℕ} - (cong fromℕ) (toℕ-fromℕ , fromℕ-toℕ) toℕ-homo-∸ +fromℕ-homo-∸ = homomorphic₂-inv ∸-magma ℕₚ.∸-magma + (cong fromℕ) toℕ-inverseᵇ toℕ-homo-∸ ------------------------------------------------------------------------ -- Properties of _∸_ and _≤_/_<_ diff --git a/src/Data/Parity/Properties.agda b/src/Data/Parity/Properties.agda index ed25a7b2fe..0c4883f08e 100644 --- a/src/Data/Parity/Properties.agda +++ b/src/Data/Parity/Properties.agda @@ -15,6 +15,7 @@ open import Data.Parity.Base as ℙ using (Parity; 0ℙ; 1ℙ; _⁻¹; toSign; f open import Data.Product using (_,_) open import Data.Sign.Base as 𝕊 open import Function hiding (Inverse) +open import Function.Consequences.Propositional open import Level using (0ℓ) open import Relation.Binary using (Decidable; DecidableEquality; Setoid; DecSetoid; IsDecEquivalence) @@ -401,6 +402,14 @@ p+p≡0ℙ 1ℙ = refl ⁻¹-homo-opposite 0ℙ = refl ⁻¹-homo-opposite 1ℙ = refl +toSign-inverseʳ : Inverseʳ _≡_ _≡_ toSign fromSign +toSign-inverseʳ {0ℙ} refl = refl +toSign-inverseʳ {1ℙ} refl = refl + +toSign-inverseˡ : Inverseˡ _≡_ _≡_ toSign fromSign +toSign-inverseˡ { + } refl = refl +toSign-inverseˡ { - } refl = refl + toSign-inverts-fromSign : ∀ {p s} → toSign p ≡ s → fromSign s ≡ p toSign-inverts-fromSign {0ℙ} refl = refl toSign-inverts-fromSign {1ℙ} refl = refl @@ -410,14 +419,10 @@ fromSign-inverts-toSign { + } refl = refl fromSign-inverts-toSign { - } refl = refl toSign-injective : Injective _≡_ _≡_ toSign -toSign-injective {p} {q} eq = begin - p ≡⟨ sym (toSign-inverts-fromSign {p} refl) ⟩ - fromSign (toSign p) ≡⟨ cong fromSign eq ⟩ - fromSign (toSign q) ≡⟨ toSign-inverts-fromSign {q} refl ⟩ - q ∎ where open ≡-Reasoning +toSign-injective = inverseʳ⇒injective toSign toSign-inverseʳ toSign-surjective : Surjective _≡_ _≡_ toSign -toSign-surjective s = (fromSign s) , fromSign-inverts-toSign {s} refl +toSign-surjective = inverseˡ⇒surjective toSign-inverseˡ toSign-isMagmaHomomorphism : IsMagmaHomomorphism ℙ.+-rawMagma 𝕊.*-rawMagma toSign toSign-isMagmaHomomorphism = record @@ -476,7 +481,7 @@ toSign-isGroupIsomorphism = record ------------------------------------------------------------------------ --- relating Nat and Parity +-- Relating Nat and Parity -- successor and (_⁻¹) diff --git a/src/Data/Product/Algebra.agda b/src/Data/Product/Algebra.agda index f11045d778..bebf6c390e 100644 --- a/src/Data/Product/Algebra.agda +++ b/src/Data/Product/Algebra.agda @@ -29,13 +29,7 @@ import Function.Definitions as FuncDef private variable a b c d p : Level - A : Set a - B : Set b - C : Set c - D : Set d - - module _ {A : Set a} {B : Set b} where - open FuncDef {A = A} {B} _≡_ _≡_ + A B C D : Set a ------------------------------------------------------------------------ -- Properties of Σ @@ -56,8 +50,8 @@ private -- × is a congruence ×-cong : A ↔ B → C ↔ D → (A × C) ↔ (B × D) ×-cong i j = mk↔′ (map I.to J.to) (map I.from J.from) - (λ {(a , b) → cong₂ _,_ (I.inverseˡ a) (J.inverseˡ b)}) - (λ {(a , b) → cong₂ _,_ (I.inverseʳ a) (J.inverseʳ b)}) + (λ {(a , b) → cong₂ _,_ (I.strictlyInverseˡ a) (J.strictlyInverseˡ b)}) + (λ {(a , b) → cong₂ _,_ (I.strictlyInverseʳ a) (J.strictlyInverseʳ b)}) where module I = Inverse i; module J = Inverse j -- × is commutative. diff --git a/src/Data/Sum/Algebra.agda b/src/Data/Sum/Algebra.agda index 717bc347c1..199dd1847d 100644 --- a/src/Data/Sum/Algebra.agda +++ b/src/Data/Sum/Algebra.agda @@ -29,14 +29,7 @@ import Function.Definitions as FuncDef private variable a b c d : Level - A : Set a - B : Set b - C : Set c - D : Set d - - -- The module is needed because we need to pass `A` and `B` to `FuncDef` - module _ {A : Set a} {B : Set b} where - open FuncDef {A = A} {B} _≡_ _≡_ + A B C D : Set a ♯ : {B : ⊥ {a} → Set b} → (w : ⊥) → B w ♯ () @@ -46,8 +39,8 @@ private ⊎-cong : A ↔ B → C ↔ D → (A ⊎ C) ↔ (B ⊎ D) ⊎-cong i j = mk↔′ (map I.to J.to) (map I.from J.from) - [ cong inj₁ ∘ I.inverseˡ , cong inj₂ ∘ J.inverseˡ ] - [ cong inj₁ ∘ I.inverseʳ , cong inj₂ ∘ J.inverseʳ ] + [ cong inj₁ ∘ I.strictlyInverseˡ , cong inj₂ ∘ J.strictlyInverseˡ ] + [ cong inj₁ ∘ I.strictlyInverseʳ , cong inj₂ ∘ J.strictlyInverseʳ ] where module I = Inverse i; module J = Inverse j -- ⊎ is commutative. diff --git a/src/Data/Vec/N-ary.agda b/src/Data/Vec/N-ary.agda index 02b6e704ba..47ab906ab2 100644 --- a/src/Data/Vec/N-ary.agda +++ b/src/Data/Vec/N-ary.agda @@ -183,5 +183,5 @@ module _ (ext : ∀ {a b} → Extensionality a b) where Vec↔N-ary (suc n) = let open Inverse (Vec↔N-ary n) in mk↔′ (λ vxs x → to λ xs → vxs (x ∷ xs)) (λ any xs → from (any (head xs)) (tail xs)) - (λ any → ext λ x → inverseˡ _) - (λ vxs → ext λ where (x ∷ xs) → cong (λ f → f xs) (inverseʳ (λ ys → vxs (x ∷ ys)))) + (λ any → ext λ x → strictlyInverseˡ _) + (λ vxs → ext λ where (x ∷ xs) → cong (λ f → f xs) (strictlyInverseʳ (λ ys → vxs (x ∷ ys)))) diff --git a/src/Data/Vec/Recursive.agda b/src/Data/Vec/Recursive.agda index 765db00991..3bd3f0b87d 100644 --- a/src/Data/Vec/Recursive.agda +++ b/src/Data/Vec/Recursive.agda @@ -44,8 +44,8 @@ private B : Set b C : Set c --- Types and patterns ------------------------------------------------------------------------ +-- Types and patterns infix 8 _^_ _^_ : Set a → ℕ → Set a @@ -61,8 +61,8 @@ a ∈[ 0 ] as = ⊥ a ∈[ 1 ] a′ = a ≡ a′ a ∈[ suc n@(suc _) ] a′ , as = a ≡ a′ ⊎ a ∈[ n ] as --- Basic operations ------------------------------------------------------------------------ +-- Basic operations cons : ∀ n → A → A ^ n → A ^ suc n cons 0 a _ = a @@ -106,9 +106,8 @@ splitAt (suc m) n xs = let (ys , zs) = splitAt m n (tail (m Nat.+ n) xs) in cons m (head (m Nat.+ n) xs) ys , zs - --- Manipulating N-ary products ------------------------------------------------------------------------ +-- Manipulating N-ary products map : (A → B) → ∀ n → A ^ n → B ^ n map f 0 as = lift tt @@ -156,7 +155,7 @@ unzip : ∀ n → (A × B) ^ n → A ^ n × B ^ n unzip = unzipWith id lift↔ : ∀ n → A ↔ B → A ^ n ↔ B ^ n -lift↔ 0 A↔B = mk↔ ((λ { [] → refl }) , (λ{ [] → refl })) +lift↔ 0 A↔B = mk↔′ _ _ (const refl) (const refl) lift↔ 1 A↔B = A↔B lift↔ (suc n@(suc _)) A↔B = ×-cong A↔B (lift↔ n A↔B) diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index 6284182845..9594a8d876 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -20,7 +20,7 @@ module Function.Bundles where open import Function.Base using (_∘_) -import Function.Definitions as FunctionDefinitions +open import Function.Definitions import Function.Structures as FunctionStructures open import Level using (Level; _⊔_; suc) open import Data.Product using (_,_; proj₁; proj₂) @@ -28,6 +28,7 @@ open import Relation.Binary hiding (_⇔_) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) import Relation.Binary.PropositionalEquality.Properties as ≡ +open import Function.Consequences.Propositional open Setoid using (isEquivalence) private @@ -42,8 +43,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where open Setoid From using () renaming (Carrier to A; _≈_ to _≈₁_) open Setoid To using () renaming (Carrier to B; _≈_ to _≈₂_) - open FunctionDefinitions _≈₁_ _≈₂_ - open FunctionStructures _≈₁_ _≈₂_ + open FunctionStructures _≈₁_ _≈₂_ ------------------------------------------------------------------------ -- Bundles with one element @@ -53,7 +53,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where record Func : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field to : A → B - cong : to Preserves _≈₁_ ⟶ _≈₂_ + cong : Congruent _≈₁_ _≈₂_ to isCongruent : IsCongruent to isCongruent = record @@ -69,8 +69,8 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where record Injection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field to : A → B - cong : to Preserves _≈₁_ ⟶ _≈₂_ - injective : Injective to + cong : Congruent _≈₁_ _≈₂_ to + injective : Injective _≈₁_ _≈₂_ to function : Func function = record @@ -91,8 +91,8 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where record Surjection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field to : A → B - cong : to Preserves _≈₁_ ⟶ _≈₂_ - surjective : Surjective to + cong : Congruent _≈₁_ _≈₂_ to + surjective : Surjective _≈₁_ _≈₂_ to to⁻ : B → A to⁻ = proj₁ ∘ surjective @@ -104,25 +104,30 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where ; isEquivalence₂ = isEquivalence To } - open IsCongruent isCongruent public using (module Eq₁; module Eq₂) - isSurjection : IsSurjection to isSurjection = record { isCongruent = isCongruent ; surjective = surjective } + open IsSurjection isSurjection public + using + ( module Eq₁ + ; module Eq₂ + ; strictlySurjective + ) + record Bijection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field to : A → B - cong : to Preserves _≈₁_ ⟶ _≈₂_ - bijective : Bijective to + cong : Congruent _≈₁_ _≈₂_ to + bijective : Bijective _≈₁_ _≈₂_ to - injective : Injective to + injective : Injective _≈₁_ _≈₂_ to injective = proj₁ bijective - surjective : Surjective to + surjective : Surjective _≈₁_ _≈₂_ to surjective = proj₂ bijective injection : Injection @@ -138,7 +143,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where } open Injection injection public using (isInjection) - open Surjection surjection public using (isSurjection; to⁻) + open Surjection surjection public using (isSurjection; to⁻; strictlySurjective) isBijection : IsBijection to isBijection = record @@ -156,7 +161,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where field to : A → B from : B → A - to-cong : to Preserves _≈₁_ ⟶ _≈₂_ + to-cong : Congruent _≈₁_ _≈₂_ to from-cong : from Preserves _≈₂_ ⟶ _≈₁_ @@ -164,9 +169,9 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where field to : A → B from : B → A - to-cong : to Preserves _≈₁_ ⟶ _≈₂_ + to-cong : Congruent _≈₁_ _≈₂_ to from-cong : from Preserves _≈₂_ ⟶ _≈₁_ - inverseˡ : Inverseˡ to from + inverseˡ : Inverseˡ _≈₁_ _≈₂_ to from isCongruent : IsCongruent to isCongruent = record @@ -175,8 +180,6 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where ; isEquivalence₂ = isEquivalence To } - open IsCongruent isCongruent public using (module Eq₁; module Eq₂) - isLeftInverse : IsLeftInverse to from isLeftInverse = record { isCongruent = isCongruent @@ -184,6 +187,9 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where ; inverseˡ = inverseˡ } + open IsLeftInverse isLeftInverse public + using (module Eq₁; module Eq₂; strictlyInverseˡ) + equivalence : Equivalence equivalence = record { to-cong = to-cong @@ -195,9 +201,9 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where field to : A → B from : B → A - to-cong : to Preserves _≈₁_ ⟶ _≈₂_ + to-cong : Congruent _≈₁_ _≈₂_ to from-cong : from Preserves _≈₂_ ⟶ _≈₁_ - inverseʳ : Inverseʳ to from + inverseʳ : Inverseʳ _≈₁_ _≈₂_ to from isCongruent : IsCongruent to isCongruent = record @@ -213,6 +219,9 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where ; inverseʳ = inverseʳ } + open IsRightInverse isRightInverse public + using (module Eq₁; module Eq₂; strictlyInverseʳ) + equivalence : Equivalence equivalence = record { to-cong = to-cong @@ -224,14 +233,14 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where field to : A → B from : B → A - to-cong : to Preserves _≈₁_ ⟶ _≈₂_ - from-cong : from Preserves _≈₂_ ⟶ _≈₁_ - inverse : Inverseᵇ to from + to-cong : Congruent _≈₁_ _≈₂_ to + from-cong : Congruent _≈₂_ _≈₁_ from + inverse : Inverseᵇ _≈₁_ _≈₂_ to from - inverseˡ : Inverseˡ to from + inverseˡ : Inverseˡ _≈₁_ _≈₂_ to from inverseˡ = proj₁ inverse - inverseʳ : Inverseʳ to from + inverseʳ : Inverseʳ _≈₁_ _≈₂_ to from inverseʳ = proj₂ inverse leftInverse : LeftInverse @@ -248,8 +257,8 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where ; inverseʳ = inverseʳ } - open LeftInverse leftInverse public using (isLeftInverse) - open RightInverse rightInverse public using (isRightInverse) + open LeftInverse leftInverse public using (isLeftInverse; strictlyInverseˡ) + open RightInverse rightInverse public using (isRightInverse; strictlyInverseʳ) isInverse : IsInverse to from isInverse = record @@ -268,21 +277,21 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where to : A → B from₁ : B → A from₂ : B → A - to-cong : to Preserves _≈₁_ ⟶ _≈₂_ - from₁-cong : from₁ Preserves _≈₂_ ⟶ _≈₁_ - from₂-cong : from₂ Preserves _≈₂_ ⟶ _≈₁_ + to-cong : Congruent _≈₁_ _≈₂_ to + from₁-cong : Congruent _≈₂_ _≈₁_ from₁ + from₂-cong : Congruent _≈₂_ _≈₁_ from₂ record BiInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field - to : A → B - from₁ : B → A - from₂ : B → A - to-cong : to Preserves _≈₁_ ⟶ _≈₂_ - from₁-cong : from₁ Preserves _≈₂_ ⟶ _≈₁_ - from₂-cong : from₂ Preserves _≈₂_ ⟶ _≈₁_ - inverseˡ : Inverseˡ to from₁ - inverseʳ : Inverseʳ to from₂ + to : A → B + from₁ : B → A + from₂ : B → A + to-cong : Congruent _≈₁_ _≈₂_ to + from₁-cong : Congruent _≈₂_ _≈₁_ from₁ + from₂-cong : Congruent _≈₂_ _≈₁_ from₂ + inverseˡ : Inverseˡ _≈₁_ _≈₂_ to from₁ + inverseʳ : Inverseʳ _≈₁_ _≈₂_ to from₂ to-isCongruent : IsCongruent to to-isCongruent = record @@ -345,29 +354,27 @@ A ↔ B = Inverse (≡.setoid A) (≡.setoid B) module _ {A : Set a} {B : Set b} where - open FunctionDefinitions {A = A} {B} _≡_ _≡_ - mk⟶ : (A → B) → A ⟶ B mk⟶ to = record { to = to ; cong = ≡.cong to } - mk↣ : ∀ {to : A → B} → Injective to → A ↣ B + mk↣ : ∀ {to : A → B} → Injective _≡_ _≡_ to → A ↣ B mk↣ {to} inj = record { to = to ; cong = ≡.cong to ; injective = inj } - mk↠ : ∀ {to : A → B} → Surjective to → A ↠ B + mk↠ : ∀ {to : A → B} → Surjective _≡_ _≡_ to → A ↠ B mk↠ {to} surj = record { to = to ; cong = ≡.cong to ; surjective = surj } - mk⤖ : ∀ {to : A → B} → Bijective to → A ⤖ B + mk⤖ : ∀ {to : A → B} → Bijective _≡_ _≡_ to → A ⤖ B mk⤖ {to} bij = record { to = to ; cong = ≡.cong to @@ -382,7 +389,7 @@ module _ {A : Set a} {B : Set b} where ; from-cong = ≡.cong from } - mk↩ : ∀ {to : A → B} {from : B → A} → Inverseˡ to from → A ↩ B + mk↩ : ∀ {to : A → B} {from : B → A} → Inverseˡ _≡_ _≡_ to from → A ↩ B mk↩ {to} {from} invˡ = record { to = to ; from = from @@ -391,7 +398,7 @@ module _ {A : Set a} {B : Set b} where ; inverseˡ = invˡ } - mk↪ : ∀ {to : A → B} {from : B → A} → Inverseʳ to from → A ↪ B + mk↪ : ∀ {to : A → B} {from : B → A} → Inverseʳ _≡_ _≡_ to from → A ↪ B mk↪ {to} {from} invʳ = record { to = to ; from = from @@ -401,7 +408,7 @@ module _ {A : Set a} {B : Set b} where } mk↩↪ : ∀ {to : A → B} {from₁ : B → A} {from₂ : B → A} → - Inverseˡ to from₁ → Inverseʳ to from₂ → A ↩↪ B + Inverseˡ _≡_ _≡_ to from₁ → Inverseʳ _≡_ _≡_ to from₂ → A ↩↪ B mk↩↪ {to} {from₁} {from₂} invˡ invʳ = record { to = to ; from₁ = from₁ @@ -413,7 +420,7 @@ module _ {A : Set a} {B : Set b} where ; inverseʳ = invʳ } - mk↔ : ∀ {to : A → B} {from : B → A} → Inverseᵇ to from → A ↔ B + mk↔ : ∀ {to : A → B} {from : B → A} → Inverseᵇ _≡_ _≡_ to from → A ↔ B mk↔ {to} {from} inv = record { to = to ; from = from @@ -422,6 +429,13 @@ module _ {A : Set a} {B : Set b} where ; inverse = inv } - -- Sometimes the implicit arguments above cannot be inferred - mk↔′ : ∀ (to : A → B) (from : B → A) → Inverseˡ to from → Inverseʳ to from → A ↔ B - mk↔′ to from invˡ invʳ = mk↔ {to = to} {from = from} (invˡ , invʳ) + -- Strict variant of the above. + mk↔′ : ∀ (to : A → B) (from : B → A) → + StrictlyInverseˡ _≡_ to from → + StrictlyInverseʳ _≡_ to from → + A ↔ B + mk↔′ to from invˡ invʳ = mk↔ {to} {from} + ( strictlyInverseˡ⇒inverseˡ to invˡ + , strictlyInverseʳ⇒inverseʳ to invʳ + ) + diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda index 2b7603deea..242aa3d289 100644 --- a/src/Function/Consequences.agda +++ b/src/Function/Consequences.agda @@ -1,56 +1,113 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Relationships between properties of functions +-- Relationships between properties of functions. See +-- `Function.Consequences.Propositional` for specialisations to +-- propositional equality. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Function.Consequences where -open import Data.Product +open import Data.Product.Base as Prod open import Function.Definitions open import Level -open import Relation.Binary -import Relation.Binary.Reasoning.Setoid as SetoidReasoning -open import Relation.Nullary.Negation using (¬_) -open import Relation.Nullary.Negation.Core using (contraposition) +open import Relation.Binary.Core +open import Relation.Binary.Definitions +open import Relation.Nullary.Negation.Core using (¬_; contraposition) private variable a b ℓ₁ ℓ₂ : Level - A : Set a - B : Set b + A B : Set a + ≈₁ ≈₂ : Rel A ℓ₁ + f f⁻¹ : A → B -module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) {f f⁻¹} where +------------------------------------------------------------------------ +-- Injective + +contraInjective : Injective ≈₁ ≈₂ f → + ∀ {x y} → ¬ (≈₁ x y) → ¬ (≈₂ (f x) (f y)) +contraInjective inj p = contraposition inj p + +------------------------------------------------------------------------ +-- Inverseˡ - inverseˡ⇒surjective : Inverseˡ ≈₁ ≈₂ f f⁻¹ → Surjective ≈₁ ≈₂ f - inverseˡ⇒surjective invˡ y = (f⁻¹ y , invˡ y) +inverseˡ⇒surjective : ∀ (≈₂ : Rel B ℓ₂) → + Inverseˡ ≈₁ ≈₂ f f⁻¹ → + Surjective ≈₁ ≈₂ f +inverseˡ⇒surjective ≈₂ invˡ y = (_ , invˡ) - inverseʳ⇒surjective : Inverseʳ ≈₁ ≈₂ f f⁻¹ → Surjective ≈₂ ≈₁ f⁻¹ - inverseʳ⇒surjective invʳ y = (f y , invʳ y) +------------------------------------------------------------------------ +-- Inverseʳ + +inverseʳ⇒injective : ∀ (≈₂ : Rel B ℓ₂) f → + Reflexive ≈₂ → + Symmetric ≈₁ → + Transitive ≈₁ → + Inverseʳ ≈₁ ≈₂ f f⁻¹ → + Injective ≈₁ ≈₂ f +inverseʳ⇒injective ≈₂ f refl sym trans invʳ {x} {y} fx≈fy = + trans (sym (invʳ refl)) (invʳ fx≈fy) -module _ (From : Setoid a ℓ₁) {≈₂ : Rel B ℓ₂} where +------------------------------------------------------------------------ +-- Inverseᵇ - open Setoid From using () renaming (Carrier to A; _≈_ to ≈₁) +inverseᵇ⇒bijective : ∀ (≈₂ : Rel B ℓ₂) → + Reflexive ≈₂ → + Symmetric ≈₁ → + Transitive ≈₁ → + Inverseᵇ ≈₁ ≈₂ f f⁻¹ → + Bijective ≈₁ ≈₂ f +inverseᵇ⇒bijective {f = f} ≈₂ refl sym trans (invˡ , invʳ) = + (inverseʳ⇒injective ≈₂ f refl sym trans invʳ , inverseˡ⇒surjective ≈₂ invˡ) - inverseʳ⇒injective : ∀ {f f⁻¹} → Congruent ≈₂ ≈₁ f⁻¹ → - Inverseʳ ≈₁ ≈₂ f f⁻¹ → Injective ≈₁ ≈₂ f - inverseʳ⇒injective {f} {f⁻¹} cong₂ invʳ {x} {y} x≈y = begin - x ≈˘⟨ invʳ x ⟩ - f⁻¹ (f x) ≈⟨ cong₂ x≈y ⟩ - f⁻¹ (f y) ≈⟨ invʳ y ⟩ - y ∎ - where open SetoidReasoning From +------------------------------------------------------------------------ +-- StrictlySurjective - inverseᵇ⇒bijective : ∀ {f f⁻¹} → Congruent ≈₂ ≈₁ f⁻¹ → Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Bijective ≈₁ ≈₂ f - inverseᵇ⇒bijective cong₂ (invˡ , invʳ) = - (inverseʳ⇒injective cong₂ invʳ , inverseˡ⇒surjective ≈₁ ≈₂ invˡ) +surjective⇒strictlySurjective : ∀ (≈₂ : Rel B ℓ₂) → + Reflexive ≈₁ → + Surjective ≈₁ ≈₂ f → + StrictlySurjective ≈₂ f +surjective⇒strictlySurjective _ refl surj x = + Prod.map₂ (λ v → v refl) (surj x) + +strictlySurjective⇒surjective : Transitive ≈₂ → + Congruent ≈₁ ≈₂ f → + StrictlySurjective ≈₂ f → + Surjective ≈₁ ≈₂ f +strictlySurjective⇒surjective trans cong surj x = + Prod.map₂ (λ fy≈x z≈y → trans (cong z≈y) fy≈x) (surj x) + +------------------------------------------------------------------------ +-- StrictlyInverseˡ + +inverseˡ⇒strictlyInverseˡ : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) → + Reflexive ≈₁ → + Inverseˡ ≈₁ ≈₂ f f⁻¹ → + StrictlyInverseˡ ≈₂ f f⁻¹ +inverseˡ⇒strictlyInverseˡ _ _ refl sinv x = sinv refl + +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ʳ -module _ - {f : A → B} (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂) - where +inverseʳ⇒strictlyInverseʳ : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) → + Reflexive ≈₂ → + Inverseʳ ≈₁ ≈₂ f f⁻¹ → + StrictlyInverseʳ ≈₁ f f⁻¹ +inverseʳ⇒strictlyInverseʳ _ _ refl sinv x = sinv refl - contraInjective : Injective _≈₁_ _≈₂_ f → - ∀ {x y} → ¬ (x ≈₁ y) → ¬ (f x ≈₂ f y) - contraInjective inj p = contraposition inj p +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) diff --git a/src/Function/Consequences/Propositional.agda b/src/Function/Consequences/Propositional.agda new file mode 100644 index 0000000000..d6067a7702 --- /dev/null +++ b/src/Function/Consequences/Propositional.agda @@ -0,0 +1,91 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Relationships between properties of functions where the equality +-- over both the domain and codomain is assumed to be _≡_ +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Function.Consequences.Propositional where + +open import Function.Definitions +open import Level +open import Relation.Nullary.Negation.Core using (contraposition) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; _≢_; refl; sym; trans; cong) + +import Function.Consequences as C + +private + variable + a b ℓ₁ ℓ₂ : Level + A B : Set a + f f⁻¹ : A → B + +------------------------------------------------------------------------ +-- Injective + +contraInjective : Injective _≡_ _≡_ f → + ∀ {x y} → x ≢ y → f x ≢ f y +contraInjective inj p = contraposition inj p + +------------------------------------------------------------------------ +-- Inverseˡ + +inverseˡ⇒surjective : Inverseˡ _≡_ _≡_ f f⁻¹ → Surjective _≡_ _≡_ f +inverseˡ⇒surjective = C.inverseˡ⇒surjective _≡_ + +------------------------------------------------------------------------ +-- Inverseʳ + +inverseʳ⇒injective : ∀ f → + Inverseʳ _≡_ _≡_ f f⁻¹ → + Injective _≡_ _≡_ f +inverseʳ⇒injective f = C.inverseʳ⇒injective _≡_ f refl sym trans + +------------------------------------------------------------------------ +-- Inverseᵇ + +inverseᵇ⇒bijective : Inverseᵇ _≡_ _≡_ f f⁻¹ → Bijective _≡_ _≡_ f +inverseᵇ⇒bijective = C.inverseᵇ⇒bijective _≡_ refl sym trans + +------------------------------------------------------------------------ +-- StrictlySurjective + +surjective⇒strictlySurjective : Surjective _≡_ _≡_ f → + StrictlySurjective _≡_ f +surjective⇒strictlySurjective = + C.surjective⇒strictlySurjective _≡_ refl + +strictlySurjective⇒surjective : StrictlySurjective _≡_ f → + Surjective _≡_ _≡_ f +strictlySurjective⇒surjective = + C.strictlySurjective⇒surjective trans (cong _) + +------------------------------------------------------------------------ +-- StrictlyInverseˡ + +inverseˡ⇒strictlyInverseˡ : Inverseˡ _≡_ _≡_ f f⁻¹ → + StrictlyInverseˡ _≡_ f f⁻¹ +inverseˡ⇒strictlyInverseˡ = + C.inverseˡ⇒strictlyInverseˡ _≡_ _≡_ refl + +strictlyInverseˡ⇒inverseˡ : ∀ f → + StrictlyInverseˡ _≡_ f f⁻¹ → + Inverseˡ _≡_ _≡_ f f⁻¹ +strictlyInverseˡ⇒inverseˡ f = + C.strictlyInverseˡ⇒inverseˡ trans (cong f) + +------------------------------------------------------------------------ +-- StrictlyInverseʳ + +inverseʳ⇒strictlyInverseʳ : Inverseʳ _≡_ _≡_ f f⁻¹ → + StrictlyInverseʳ _≡_ f f⁻¹ +inverseʳ⇒strictlyInverseʳ = C.inverseʳ⇒strictlyInverseʳ _≡_ _≡_ refl + +strictlyInverseʳ⇒inverseʳ : ∀ f → + StrictlyInverseʳ _≡_ f f⁻¹ → + Inverseʳ _≡_ _≡_ f f⁻¹ +strictlyInverseʳ⇒inverseʳ {f⁻¹ = f⁻¹} _ = + C.strictlyInverseʳ⇒inverseʳ trans (cong f⁻¹) diff --git a/src/Function/Construct/Composition.agda b/src/Function/Construct/Composition.agda index f6588af99f..08c2250dcd 100644 --- a/src/Function/Construct/Composition.agda +++ b/src/Function/Construct/Composition.agda @@ -49,11 +49,11 @@ module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) (≈₃ : Rel C ℓ₃) inverseˡ : Inverseˡ ≈₁ ≈₂ f f⁻¹ → Inverseˡ ≈₂ ≈₃ g g⁻¹ → Inverseˡ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹) - inverseˡ f-inv g-inv x y≈gfx = g-inv x (f-inv (g⁻¹ x) y≈gfx) + inverseˡ f-inv g-inv = g-inv ∘ f-inv inverseʳ : Inverseʳ ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₂ ≈₃ g g⁻¹ → Inverseʳ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹) - inverseʳ f-inv g-inv x y≈gfx = f-inv x (g-inv (f x) y≈gfx) + inverseʳ f-inv g-inv = f-inv ∘ g-inv inverseᵇ : Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Inverseᵇ ≈₂ ≈₃ g g⁻¹ → Inverseᵇ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹) diff --git a/src/Function/Construct/Identity.agda b/src/Function/Construct/Identity.agda index b83cd16ad1..46fd351dd2 100644 --- a/src/Function/Construct/Identity.agda +++ b/src/Function/Construct/Identity.agda @@ -27,27 +27,27 @@ private module _ (_≈_ : Rel A ℓ) where - open Definitions _≈_ _≈_ + open Definitions - congruent : Congruent id + congruent : Congruent _≈_ _≈_ id congruent = id - injective : Injective id + injective : Injective _≈_ _≈_ id injective = id - surjective : Surjective id + surjective : Surjective _≈_ _≈_ id surjective x = x , id - bijective : Bijective id + bijective : Bijective _≈_ _≈_ id bijective = injective , surjective - inverseˡ : Inverseˡ id id - inverseˡ x = id + inverseˡ : Inverseˡ _≈_ _≈_ id id + inverseˡ = id - inverseʳ : Inverseʳ id id - inverseʳ x = id + inverseʳ : Inverseʳ _≈_ _≈_ id id + inverseʳ = id - inverseᵇ : Inverseᵇ id id + inverseᵇ : Inverseᵇ _≈_ _≈_ id id inverseᵇ = inverseˡ , inverseʳ ------------------------------------------------------------------------ diff --git a/src/Function/Definitions.agda b/src/Function/Definitions.agda index 15eee5c859..27a423ad5b 100644 --- a/src/Function/Definitions.agda +++ b/src/Function/Definitions.agda @@ -8,37 +8,57 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary +module Function.Definitions where -module Function.Definitions - {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} +open import Data.Product using (∃; _×_) +open import Level using (Level) +open import Relation.Binary.Core using (Rel) + +private + variable + a ℓ₁ ℓ₂ : Level + A B : Set a + +------------------------------------------------------------------------ +-- Basic definitions + +module _ (_≈₁_ : Rel A ℓ₁) -- Equality over the domain (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain where -open import Data.Product using (∃; _×_) -open import Level using (_⊔_) + Congruent : (A → B) → Set _ + Congruent f = ∀ {x y} → x ≈₁ y → f x ≈₂ f y ------------------------------------------------------------------------- --- Definitions + Injective : (A → B) → Set _ + Injective f = ∀ {x y} → f x ≈₂ f y → x ≈₁ y + + Surjective : (A → B) → Set _ + Surjective f = ∀ y → ∃ λ x → ∀ {z} → z ≈₁ x → f z ≈₂ y + + Bijective : (A → B) → Set _ + Bijective f = Injective f × Surjective f -Congruent : (A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂) -Congruent f = ∀ {x y} → x ≈₁ y → f x ≈₂ f y + Inverseˡ : (A → B) → (B → A) → Set _ + Inverseˡ f g = ∀ {x y} → y ≈₁ g x → f y ≈₂ x -Injective : (A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂) -Injective f = ∀ {x y} → f x ≈₂ f y → x ≈₁ y + Inverseʳ : (A → B) → (B → A) → Set _ + Inverseʳ f g = ∀ {x y} → y ≈₂ f x → g y ≈₁ x -Surjective : (A → B) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) -Surjective f = ∀ y → ∃ λ x → ∀ {z} → z ≈₁ x → f z ≈₂ y + Inverseᵇ : (A → B) → (B → A) → Set _ + Inverseᵇ f g = Inverseˡ f g × Inverseʳ f g + +------------------------------------------------------------------------ +-- Strict definitions -Bijective : (A → B) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) -Bijective f = Injective f × Surjective f +-- These are often easier to use once but much harder to compose and +-- reason about. -Inverseˡ : (A → B) → (B → A) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) -Inverseˡ f g = ∀ x {y} → y ≈₁ g x → f y ≈₂ x +StrictlySurjective : Rel B ℓ₂ → (A → B) → Set _ +StrictlySurjective _≈₂_ f = ∀ y → ∃ λ x → f x ≈₂ y -Inverseʳ : (A → B) → (B → A) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) -Inverseʳ f g = ∀ x {y} → y ≈₂ f x → g y ≈₁ x +StrictlyInverseˡ : Rel B ℓ₂ → (A → B) → (B → A) → Set _ +StrictlyInverseˡ _≈₂_ f g = ∀ y → f (g y) ≈₂ y -Inverseᵇ : (A → B) → (B → A) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) -Inverseᵇ f g = Inverseˡ f g × Inverseʳ f g +StrictlyInverseʳ : Rel A ℓ₁ → (A → B) → (B → A) → Set _ +StrictlyInverseʳ _≈₁_ f g = ∀ x → g (f x) ≈₁ x diff --git a/src/Function/Properties.agda b/src/Function/Properties.agda index b20807f64e..6b8ee782f6 100644 --- a/src/Function/Properties.agda +++ b/src/Function/Properties.agda @@ -42,6 +42,6 @@ private →-cong-↔ extAC extBD A↔B C↔D = mk↔′ (λ h → C↔D.to ∘ h ∘ A↔B.from) (λ g → C↔D.from ∘ g ∘ A↔B.to ) - (λ h → extBD λ x → trans (C↔D.inverseˡ _) (cong h (A↔B.inverseˡ x))) - (λ g → extAC λ x → trans (C↔D.inverseʳ _) (cong g (A↔B.inverseʳ x))) + (λ h → extBD λ x → trans (C↔D.strictlyInverseˡ _) (cong h (A↔B.strictlyInverseˡ x))) + (λ g → extAC λ x → trans (C↔D.strictlyInverseʳ _) (cong g (A↔B.strictlyInverseʳ x))) where module A↔B = Inverse A↔B; module C↔D = Inverse C↔D diff --git a/src/Function/Properties/Bijection.agda b/src/Function/Properties/Bijection.agda index e484098774..1f76695ff2 100644 --- a/src/Function/Properties/Bijection.agda +++ b/src/Function/Properties/Bijection.agda @@ -12,9 +12,9 @@ open import Function.Bundles open import Level using (Level) open import Relation.Binary hiding (_⇔_) open import Relation.Binary.PropositionalEquality as P using (setoid) -import Relation.Binary.Reasoning.Setoid as SetoidReasoning open import Data.Product 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) import Function.Construct.Identity as Identity @@ -55,18 +55,15 @@ trans = Composition.bijection -- Conversion functions Bijection⇒Inverse : Bijection S T → Inverse S T -Bijection⇒Inverse {S = S} {T = T} b = record +Bijection⇒Inverse bij = record { to = to ; from = to⁻ ; to-cong = cong - ; from-cong = λ {x} {y} x≈y → injective (begin - to (to⁻ x) ≈⟨ to∘to⁻ x ⟩ - x ≈⟨ x≈y ⟩ - y ≈˘⟨ to∘to⁻ y ⟩ - to (to⁻ y) ∎) - ; inverse = to∘to⁻ , injective ∘ to∘to⁻ ∘ to + ; 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 SetoidReasoning T; open Bijection b; to∘to⁻ = proj₂ ∘ surjective + where open Bijection bij; to∘to⁻ = proj₂ ∘ strictlySurjective Bijection⇒Equivalence : Bijection T S → Equivalence T S Bijection⇒Equivalence = Inverse⇒Equivalence ∘ Bijection⇒Inverse diff --git a/src/Function/Properties/Inverse.agda b/src/Function/Properties/Inverse.agda index 6310a8479f..ccdc559553 100644 --- a/src/Function/Properties/Inverse.agda +++ b/src/Function/Properties/Inverse.agda @@ -56,17 +56,17 @@ open module ↔ {ℓ} = IsEquivalence (↔-isEquivalence {ℓ}) using () -- Conversion functions Inverse⇒Injection : Inverse S T → Injection S T -Inverse⇒Injection {S = S} I = record +Inverse⇒Injection I = record { to = to ; cong = to-cong - ; injective = inverseʳ⇒injective S {f⁻¹ = from} from-cong inverseʳ + ; injective = inverseʳ⇒injective Eq₂._≈_ to Eq₂.refl Eq₁.sym Eq₁.trans inverseʳ } where open Inverse I Inverse⇒Bijection : Inverse S T → Bijection S T -Inverse⇒Bijection {S = S} I = record +Inverse⇒Bijection I = record { to = to ; cong = to-cong - ; bijective = inverseᵇ⇒bijective S from-cong inverse + ; bijective = inverseᵇ⇒bijective Eq₂._≈_ Eq₂.refl Eq₁.sym Eq₁.trans inverse } where open Inverse I Inverse⇒Equivalence : Inverse S T → Equivalence S T @@ -92,6 +92,6 @@ module _ (ext : ∀ {a b} → Extensionality a b) where ↔-fun A↔B C↔D = mk↔′ (λ a→c b → to C↔D (a→c (from A↔B b))) (λ b→d a → from C↔D (b→d (to A↔B a))) - (λ b→d → ext λ _ → P.trans (inverseˡ C↔D _ ) (P.cong b→d (inverseˡ A↔B _))) - (λ a→c → ext λ _ → P.trans (inverseʳ C↔D _ ) (P.cong a→c (inverseʳ A↔B _))) + (λ b→d → ext λ _ → P.trans (strictlyInverseˡ C↔D _ ) (P.cong b→d (strictlyInverseˡ A↔B _))) + (λ a→c → ext λ _ → P.trans (strictlyInverseʳ C↔D _ ) (P.cong a→c (strictlyInverseʳ A↔B _))) where open Inverse diff --git a/src/Function/Properties/RightInverse.agda b/src/Function/Properties/RightInverse.agda index f5aa05d9df..66b35e53f0 100644 --- a/src/Function/Properties/RightInverse.agda +++ b/src/Function/Properties/RightInverse.agda @@ -10,7 +10,7 @@ module Function.Properties.RightInverse where open import Function.Base open import Function.Bundles -open import Function.Consequences using (inverseʳ⇒surjective) +open import Function.Consequences using (inverseˡ⇒surjective) open import Level using (Level) open import Data.Product open import Relation.Binary using (Setoid; IsEquivalence) @@ -27,7 +27,7 @@ RightInverse⇒Surjection : RightInverse S T → Surjection T S RightInverse⇒Surjection I = record { to = from ; cong = from-cong - ; surjective = λ a → to a , inverseʳ a + ; surjective = inverseˡ⇒surjective Eq₁._≈_ inverseʳ } where open RightInverse I ↪⇒↠ : B ↪ A → A ↠ B diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda index ab164c43d0..fce294be76 100644 --- a/src/Function/Properties/Surjection.agda +++ b/src/Function/Properties/Surjection.agda @@ -9,20 +9,39 @@ module Function.Properties.Surjection where open import Function.Base +open import Function.Definitions open import Function.Bundles open import Level using (Level) open import Data.Product +open import Relation.Binary.PropositionalEquality +open import Relation.Binary using (Setoid) +import Relation.Binary.Reasoning.Setoid as SetoidReasoning private variable - a b : Level + a b ℓ : Level A B : Set a + T S : Setoid a ℓ + +injective⇒to⁻-cong : (surj : Surjection S T) → + (open Surjection surj) → + Injective Eq₁._≈_ Eq₂._≈_ to → + Congruent Eq₂._≈_ Eq₁._≈_ to⁻ +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) ∎ + where + open SetoidReasoning T + open Surjection surj + to∘to⁻ = proj₂ ∘ strictlySurjective ------------------------------------------------------------------------ -- Conversion functions ↠⇒↪ : A ↠ B → B ↪ A -↠⇒↪ s = mk↪ {to = proj₁ ∘ surjective} {from = to} (proj₂ ∘ surjective) +↠⇒↪ s = mk↪ {from = to} λ { refl → proj₂ (strictlySurjective _)} where open Surjection s ↠⇒⇔ : A ↠ B → A ⇔ B diff --git a/src/Function/Related.agda b/src/Function/Related.agda index 0746b3c14a..6d2d85d49d 100644 --- a/src/Function/Related.agda +++ b/src/Function/Related.agda @@ -17,6 +17,7 @@ open import Function.Injection as Inj using (Injection; _↣_) open import Function.Inverse as Inv using (Inverse; _↔_) open import Function.LeftInverse as LeftInv using (LeftInverse) open import Function.Surjection as Surj using (Surjection) +open import Function.Consequences.Propositional open import Relation.Binary open import Relation.Binary.PropositionalEquality as P using (_≡_) open import Data.Product using (_,_; proj₁; proj₂; <_,_>) @@ -91,12 +92,12 @@ toRelated {K = reverse-implication} rel = lam (B.Func.to rel) toRelated {K = equivalence} rel = Eq.equivalence (B.Equivalence.to rel) (B.Equivalence.from rel) toRelated {K = injection} rel = Inj.injection (B.Injection.to rel) (B.Injection.injective rel) toRelated {K = reverse-injection} rel = lam (Inj.injection (B.Injection.to rel) (B.Injection.injective rel)) -toRelated {K = left-inverse} rel = - LeftInv.leftInverse (B.RightInverse.to rel) (B.RightInverse.from rel) (B.RightInverse.inverseʳ rel) -toRelated {K = surjection} rel with B.Surjection.surjective rel -... | surj = Surj.surjection (B.Surjection.to rel) (proj₁ ∘ surj) (proj₂ ∘ surj) -toRelated {K = bijection} rel with B.Bijection.bijective rel -... | (inj , surj) = Inv.inverse (B.Bijection.to rel) (proj₁ ∘ surj) (inj ∘ proj₂ ∘ surj ∘ (B.Bijection.to rel)) (proj₂ ∘ surj) +toRelated {K = left-inverse} rel = LeftInv.leftInverse to from strictlyInverseʳ where open B.RightInverse rel +toRelated {K = surjection} rel = Surj.surjection to (proj₁ ∘ strictlySurjective) (proj₂ ∘ strictlySurjective) + where open B.Surjection rel +toRelated {K = bijection} rel = + Inv.inverse to (proj₁ ∘ strictlySurjective) (injective ∘ proj₂ ∘ strictlySurjective ∘ to) (proj₂ ∘ strictlySurjective) + where open B.Bijection rel fromRelated : {K : Kind} → A ∼[ K ] B → A R.∼[ K ] B fromRelated {K = implication} rel = B.mk⟶ rel @@ -105,13 +106,14 @@ fromRelated {K = equivalence} record { to = to ; from = from } = B.mk⇔ fromRelated {K = injection} rel = B.mk↣ (Inj.Injection.injective rel) fromRelated {K = reverse-injection} (lam app-↢) = B.mk↣ (Inj.Injection.injective app-↢) fromRelated {K = left-inverse} record { to = to ; from = from ; left-inverse-of = left-inverse-of } = - B.mk↪ {to = to ⟨$⟩_} {from = from ⟨$⟩_} left-inverse-of + B.mk↪ {to = to ⟨$⟩_} {from = from ⟨$⟩_} (strictlyInverseʳ⇒inverseʳ (to ⟨$⟩_) left-inverse-of) fromRelated {K = surjection} record { to = to ; surjective = surjective } with surjective -... | record { from = from ; right-inverse-of = right-inverse-of } = B.mk↠ {to = to ⟨$⟩_} < from ⟨$⟩_ , right-inverse-of > +... | record { from = from ; right-inverse-of = right-inverse-of } = + B.mk↠ {to = to ⟨$⟩_} < from ⟨$⟩_ , (λ { x P.refl → right-inverse-of x }) > fromRelated {K = bijection} record { to = to ; from = from ; inverse-of = inverse-of } with inverse-of ... | record { left-inverse-of = left-inverse-of ; right-inverse-of = right-inverse-of } = B.mk⤖ ((λ {x y} h → P.subst₂ P._≡_ (left-inverse-of x) (left-inverse-of y) (P.cong (from ⟨$⟩_) h)) , - < from ⟨$⟩_ , right-inverse-of >) + < from ⟨$⟩_ , (λ { x P.refl → right-inverse-of x }) >) -- A non-infix synonym. diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index 52fe836abd..4d8d953755 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -18,6 +18,7 @@ module Function.Structures {a b ℓ₁ ℓ₂} open import Data.Product as Product using (∃; _×_; _,_) open import Function.Base open import Function.Definitions +open import Function.Consequences open import Level using (_⊔_) ------------------------------------------------------------------------ @@ -64,7 +65,7 @@ record IsSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where open IsCongruent isCongruent public - strictlySurjective : ∀ y → ∃ λ x → f x ≈₂ y + strictlySurjective : StrictlySurjective _≈₂_ f strictlySurjective x = Product.map₂ (λ v → v Eq₁.refl) (surjective x) @@ -101,8 +102,8 @@ record IsLeftInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ open IsCongruent isCongruent public renaming (cong to to-cong) - strictInverseˡ : ∀ x → to (from x) ≈₂ x - strictInverseˡ x = inverseˡ x Eq₁.refl + strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from + strictlyInverseˡ x = inverseˡ Eq₁.refl record IsRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where @@ -114,8 +115,8 @@ record IsRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ open IsCongruent isCongruent public renaming (cong to cong₁) - strictInverseʳ : ∀ x → from (to x) ≈₁ x - strictInverseʳ x = inverseʳ x Eq₂.refl + strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from + strictlyInverseʳ x = inverseʳ Eq₂.refl record IsInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where @@ -133,7 +134,7 @@ record IsInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ } open IsRightInverse isRightInverse public - using (strictInverseʳ) + using (strictlyInverseʳ) inverse : Inverseᵇ _≈₁_ _≈₂_ to from inverse = inverseˡ , inverseʳ diff --git a/src/Relation/Binary/Morphism/Construct/Composition.agda b/src/Relation/Binary/Morphism/Construct/Composition.agda index 202605b608..5f6fe9bf32 100644 --- a/src/Relation/Binary/Morphism/Construct/Composition.agda +++ b/src/Relation/Binary/Morphism/Construct/Composition.agda @@ -46,9 +46,9 @@ isRelIsomorphism : Transitive ≈₃ → IsRelIsomorphism ≈₁ ≈₂ f → IsRelIsomorphism ≈₂ ≈₃ g → IsRelIsomorphism ≈₁ ≈₃ (g ∘ f) -isRelIsomorphism {≈₁ = ≈₁} ≈₃-trans m₁ m₂ = record +isRelIsomorphism {≈₃ = ≈₃} ≈₃-trans m₁ m₂ = record { isMonomorphism = isRelMonomorphism F.isMonomorphism G.isMonomorphism - ; surjective = surjective ≈₁ _ _ ≈₃-trans G.cong F.surjective G.surjective + ; surjective = surjective _ _ ≈₃ F.surjective G.surjective } where module F = IsRelIsomorphism m₁; module G = IsRelIsomorphism m₂ ------------------------------------------------------------------------ @@ -103,9 +103,9 @@ isOrderIsomorphism : Transitive ≈₃ → IsOrderIsomorphism ≈₁ ≈₂ ∼₁ ∼₂ f → IsOrderIsomorphism ≈₂ ≈₃ ∼₂ ∼₃ g → IsOrderIsomorphism ≈₁ ≈₃ ∼₁ ∼₃ (g ∘ f) -isOrderIsomorphism {≈₁ = ≈₁} ≈₃-trans m₁ m₂ = record +isOrderIsomorphism {≈₃ = ≈₃} ≈₃-trans m₁ m₂ = record { isOrderMonomorphism = isOrderMonomorphism F.isOrderMonomorphism G.isOrderMonomorphism - ; surjective = surjective ≈₁ _ _ ≈₃-trans G.cong F.surjective G.surjective + ; surjective = surjective _ _ ≈₃ F.surjective G.surjective } where module F = IsOrderIsomorphism m₁; module G = IsOrderIsomorphism m₂ ------------------------------------------------------------------------ diff --git a/src/Relation/Binary/Morphism/Construct/Identity.agda b/src/Relation/Binary/Morphism/Construct/Identity.agda index c8ed9c6b03..24ba69d1e4 100644 --- a/src/Relation/Binary/Morphism/Construct/Identity.agda +++ b/src/Relation/Binary/Morphism/Construct/Identity.agda @@ -8,6 +8,7 @@ open import Data.Product using (_,_) open import Function.Base using (id) +import Function.Construct.Identity as Id open import Level using (Level) open import Relation.Binary open import Relation.Binary.Morphism.Structures @@ -29,19 +30,19 @@ module _ (≈ : Rel A ℓ₁) where isRelHomomorphism : IsRelHomomorphism ≈ ≈ id isRelHomomorphism = record - { cong = id + { cong = Id.congruent ≈ } isRelMonomorphism : IsRelMonomorphism ≈ ≈ id isRelMonomorphism = record { isHomomorphism = isRelHomomorphism - ; injective = id + ; injective = Id.injective ≈ } isRelIsomorphism : Reflexive ≈ → IsRelIsomorphism ≈ ≈ id isRelIsomorphism refl = record { isMonomorphism = isRelMonomorphism - ; surjective = λ y → y , refl + ; surjective = Id.surjective ≈ } ------------------------------------------------------------------------ @@ -76,14 +77,14 @@ module _ (≈ : Rel A ℓ₁) (∼ : Rel A ℓ₂) where isOrderMonomorphism : IsOrderMonomorphism ≈ ≈ ∼ ∼ id isOrderMonomorphism = record { isOrderHomomorphism = isOrderHomomorphism - ; injective = id + ; injective = Id.injective ≈ ; cancel = id } isOrderIsomorphism : Reflexive ≈ → IsOrderIsomorphism ≈ ≈ ∼ ∼ id isOrderIsomorphism refl = record { isOrderMonomorphism = isOrderMonomorphism - ; surjective = λ y → y , refl + ; surjective = Id.surjective ≈ } ------------------------------------------------------------------------ From 51849ba19a7384c19cac61cddf06fa1bdf8bc40a Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Sat, 10 Jun 2023 17:05:58 +0900 Subject: [PATCH 4/4] Added CHANGELOG entry --- CHANGELOG.md | 41 ++++++++++++++++++++++++++++++--- src/Data/Parity/Properties.agda | 8 ------- 2 files changed, 38 insertions(+), 11 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 52b2a6762d..79602c24b9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -179,7 +179,7 @@ Non-backwards compatible changes * Added new aliases `Is(Meet/Join)(Bounded)Semilattice` for `Is(Bounded)Semilattice` which can be used to indicate meet/join-ness of the original structures. -#### Function hierarchy +#### Removal of the old function hierarchy * The switch to the new function hierarchy is complete and the following definitions now use the new definitions instead of the old ones: @@ -252,9 +252,41 @@ Non-backwards compatible changes * `Relation.Nullary.Decidable` * `map` -* The names of the fields in the records of the new hierarchy have been - changed from `f`, `g`, `cong₁`, `cong₂` to `to`, `from`, `to-cong`, `from-cong`. +#### Changes to the new function hierarchy + +* The names of the fields in `Function.Bundles` have been + changed from `f`, `g`, `cong₁` and `cong₂` to `to`, `from`, `to-cong`, `from-cong`. + +* The module `Function.Definitions` no longer has two equalities as module arguments, as + they did not interact as intended with the re-exports from `Function.Definitions.(Core1/Core2)`. + The latter have been removed and their definitions folded into `Function.Definitions`. + +* In `Function.Definitions` the types of `Surjective`, `Injective` and `Surjective` + have been changed from: + ``` + Surjective f = ∀ y → ∃ λ x → f x ≈₂ y + Inverseˡ f g = ∀ y → f (g y) ≈₂ y + Inverseʳ f g = ∀ x → g (f x) ≈₁ x + ``` + to: + ``` + Surjective f = ∀ y → ∃ λ x → ∀ {z} → z ≈₁ x → f z ≈₂ y + Inverseˡ f g = ∀ {x y} → y ≈₁ g x → f y ≈₂ x + Inverseʳ f g = ∀ {x y} → y ≈₂ f x → g y ≈₁ x + ``` + This is for several reasons: i) the new definitions compose much more easily, ii) Agda + can better infer the equalities used. + + To ease backwards compatibility: + - the old definitions have been moved to the new names `StrictlySurjective`, + `StrictlyInverseˡ` and `StrictlyInverseʳ`. + - The records in `Function.Structures` and `Function.Bundles` export proofs + of these under the names `strictlySurjective`, `strictlyInverseˡ` and + `strictlyInverseʳ`, + - Conversion functions have been added in both directions to + `Function.Consequences(.Propositional)`. + #### Proofs of non-zeroness/positivity/negativity as instance arguments * Many numeric operations in the library require their arguments to be non-zero, @@ -2057,6 +2089,9 @@ Other minor changes * Added a new proof to `Data.Nat.Binary.Properties`: ```agda suc-injective : Injective _≡_ _≡_ suc + toℕ-inverseˡ : Inverseˡ _≡_ _≡_ toℕ fromℕ + toℕ-inverseʳ : Inverseʳ _≡_ _≡_ toℕ fromℕ + toℕ-inverseᵇ : Inverseᵇ _≡_ _≡_ toℕ fromℕ ``` * Added new definitions and proofs to `Data.Nat.Primality`: diff --git a/src/Data/Parity/Properties.agda b/src/Data/Parity/Properties.agda index 0c4883f08e..7466572a77 100644 --- a/src/Data/Parity/Properties.agda +++ b/src/Data/Parity/Properties.agda @@ -410,14 +410,6 @@ toSign-inverseˡ : Inverseˡ _≡_ _≡_ toSign fromSign toSign-inverseˡ { + } refl = refl toSign-inverseˡ { - } refl = refl -toSign-inverts-fromSign : ∀ {p s} → toSign p ≡ s → fromSign s ≡ p -toSign-inverts-fromSign {0ℙ} refl = refl -toSign-inverts-fromSign {1ℙ} refl = refl - -fromSign-inverts-toSign : ∀ {s p} → fromSign s ≡ p → toSign p ≡ s -fromSign-inverts-toSign { + } refl = refl -fromSign-inverts-toSign { - } refl = refl - toSign-injective : Injective _≡_ _≡_ toSign toSign-injective = inverseʳ⇒injective toSign toSign-inverseʳ