Change Function.Definitions to use strict inverses (#1156)

CHANGELOG.md

@@ -272,7 +272,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:
@@ -345,9 +345,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,
@@ -2206,6 +2238,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 a new pattern synonym to `Data.Nat.Divisibility.Core`:

src/Algebra/Consequences/Setoid.agda

@@ -19,8 +19,8 @@ open import Algebra.Core
 open import Algebra.Definitions _≈_
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Product.Base 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)
@@ -67,45 +67,32 @@ module _ {_•_ : Op₂ A} (cong : Congruent₂ _•_) where
  y • x ∎
 
 ------------------------------------------------------------------------
--- 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
 
 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
 
 ------------------------------------------------------------------------

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

src/Algebra/Lattice/Morphism/Construct/Identity.agda

@@ -13,6 +13,7 @@ open import Algebra.Lattice.Morphism.Structures
  using ( module LatticeMorphisms )
 open import Data.Product.Base 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 _
  }

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
 

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

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.Base 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 _
  }