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

Author: alexarice

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