[ refactor ] fixes #2568; proves full symmetry for Bijection

CHANGELOG.md

@@ -6,6 +6,11 @@ The library has been tested using Agda 2.7.0 and 2.7.0.1.
 Highlights
 ----------
 
+* A major overhaul of the `Function` hierarchy sees the systematic development
+  and use of theory of the left inverse `from` to a given `Surjective` function
+  `to`, in `Function.Consequences.Section`, up to and including full symmetry of
+  `Bijection`, in `Function.Properties.Bijection`.
+
 Bug-fixes
 ---------
 
@@ -57,6 +62,32 @@ Deprecated names
   or        ↦  Data.Bool.ListAction.or
   any       ↦  Data.Bool.ListAction.any
   all       ↦  Data.Bool.ListAction.all
+ ```
+
+* In `Function.Bundles.IsSurjection`:
+  ```agda
+  to⁻      ↦  Function.Structures.IsSurjection.from
+  to∘to⁻   ↦  Function.Structures.IsSurjection.strictlyInverseˡ
+  ```
+
+* In `Function.Construct.Symmetry`:
+  ```agda
+  injective       ↦  Function.Consequences.Section.injective
+  surjective      ↦  Function.Consequences.Section.surjective
+  bijective       ↦  Function.Consequences.Section.bijective
+  isBijection     ↦  isBijectionWithoutCongruence
+  isBijection-≡   ↦  isBijectionWithoutCongruence
+  bijection-≡     ↦  bijectionWithoutCongruence
+  ```
+
+* In `Function.Properties.Bijection`:
+  ```agda
+  sym-≡   ↦  sym
+  ```
+
+* In `Function.Properties.Surjection`:
+  ```agda
+  injective⇒to⁻-cong   ↦  Function.Construct.Symmetry.bijectionWithoutCongruence
   ```
 
 New modules
@@ -95,3 +126,77 @@ Additions to existing modules
   quasiring                       : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ)
   commutativeRing                 : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
   ```
+
+* In `Function.Bundles.Bijection`:
+  ```agda
+  from             : B → A
+  inverseˡ         : Inverseˡ _≈₁_ _≈₂_ to from
+  strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from
+  inverseʳ         : Inverseʳ _≈₁_ _≈₂_ to from
+  strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from
+  ```
+
+* In `Function.Bundles.LeftInverse`:
+  ```agda
+  surjective       : Surjective _≈₁_ _≈₂_ to
+  surjection       : Surjection From To
+  ```
+
+* In `Function.Bundles.RightInverse`:
+  ```agda
+  isInjection      : IsInjection to
+  injective        : Injective _≈₁_ _≈₂_ to
+  injection        : Injection From To
+  ```
+
+* In `Function.Bundles.Surjection`:
+  ```agda
+  from             : B → A
+  inverseˡ         : Inverseˡ _≈₁_ _≈₂_ to from
+  strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from
+  ```
+
+* In `Function.Consequences` and `Function.Consequences.Setoid`:
+  the theory of the left inverse of a surjective function `to`
+  ```agda
+  module Section (surj :  Surjective ≈₁ ≈₂ to)
+  ```
+
+* In `Function.Construct.Symmetry`:
+  ```agda
+  isBijectionWithoutCongruence : IsBijection ≈₁ ≈₂ to → IsBijection ≈₂ ≈₁ from
+  bijectionWithoutCongruence   : Bijection R S → Bijection S R
+  ```
+
+* In `Function.Properties.Bijection`:
+  ```agda
+  sym : Bijection S T → Bijection T S
+  ```
+
+* In `Function.Structures.IsBijection`:
+  ```agda
+  from             : B → A
+  inverseˡ         : Inverseˡ _≈₁_ _≈₂_ to from
+  strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from
+  inverseʳ         : Inverseʳ _≈₁_ _≈₂_ to from
+  strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from
+  ```
+
+* In `Function.Structures.IsLeftInverse`:
+  ```agda
+  surjective : Surjective _≈₁_ _≈₂_ to
+  ```
+
+* In `Function.Structures.IsRightInverse`:
+  ```agda
+  injective   : Injective _≈₁_ _≈₂_ to
+  isInjection : IsInjection to
+  ```
+
+* In `Function.Structures.IsSurjection`:
+  ```agda
+  from          : B → A
+  inverseˡ         : Inverseˡ _≈₁_ _≈₂_ to from
+  strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from
+  ```
+

src/Data/Product/Function/Dependent/Propositional.agda

@@ -57,7 +57,7 @@ module _ where
          Σ I A ⇔ Σ J B
   Σ-⇔ {B = B} I↠J A⇔B = mk⇔
     (map (to  I↠J) (Equivalence.to A⇔B))
-    (map (to⁻ I↠J) (Equivalence.from A⇔B ∘ ≡.subst B (≡.sym (proj₂ (surjective I↠J _) ≡.refl))))
+    (map (from I↠J) (Equivalence.from A⇔B ∘ ≡.subst B (≡.sym (proj₂ (surjective I↠J _) ≡.refl))))
 
   -- See also Data.Product.Relation.Binary.Pointwise.Dependent.WithK.↣.
 
@@ -193,18 +193,22 @@ module _ where
     to′ : Σ I A → Σ J B
     to′ = map (to I↠J) (to A↠B)
 
-    backcast : ∀ {i} → B i → B (to I↠J (to⁻ I↠J i))
-    backcast = ≡.subst B (≡.sym (to∘to⁻ I↠J _))
+    backcast : ∀ {i} → B i → B (to I↠J (from I↠J i))
+    backcast = ≡.subst B (≡.sym (strictlyInverseˡ I↠J _))
 
-    to⁻′ : Σ J B → Σ I A
-    to⁻′ = map (to⁻ I↠J) (Surjection.to⁻ A↠B ∘ backcast)
+    from′ : Σ J B → Σ I A
+    from′ = map (from I↠J) (from A↠B ∘ backcast)
 
     strictlySurjective′ : StrictlySurjective _≡_ to′
-    strictlySurjective′ (x , y) = to⁻′ (x , y) , Σ-≡,≡→≡
-      ( to∘to⁻ I↠J x
-      , (≡.subst B (to∘to⁻ I↠J x) (to A↠B (to⁻ A↠B (backcast y))) ≡⟨ ≡.cong (≡.subst B _) (to∘to⁻ A↠B _) ⟩
-         ≡.subst B (to∘to⁻ I↠J x) (backcast y)                      ≡⟨ ≡.subst-subst-sym (to∘to⁻ I↠J x) ⟩
-         y                                                          ∎)
+    strictlySurjective′ (x , y) = from′ (x , y) , Σ-≡,≡→≡
+      ( strictlyInverseˡ I↠J x
+      , (begin
+           ≡.subst B (strictlyInverseˡ I↠J x) (to A↠B (from A↠B (backcast y)))
+             ≡⟨ ≡.cong (≡.subst B _) (strictlyInverseˡ A↠B _) ⟩
+           ≡.subst B (strictlyInverseˡ I↠J x) (backcast y)
+             ≡⟨ ≡.subst-subst-sym (strictlyInverseˡ I↠J x) ⟩
+           y
+             ∎)
       ) where open ≡.≡-Reasoning
 
 
@@ -249,8 +253,8 @@ module _ where
       Σ I A ↔ Σ J B
   Σ-↔ {I = I} {J = J} {A = A} {B = B} I↔J A↔B = mk↔ₛ′
     (Surjection.to surjection′)
-    (Surjection.to⁻ surjection′)
-    (Surjection.to∘to⁻ surjection′)
+    (Surjection.from surjection′)
+    (Surjection.strictlyInverseˡ surjection′)
     left-inverse-of
     where
     open ≡.≡-Reasoning
@@ -260,7 +264,7 @@ module _ where
     surjection′ : Σ I A ↠ Σ J B
     surjection′ = Σ-↠ (↔⇒↠ (≃⇒↔ I≃J)) (↔⇒↠ A↔B)
 
-    left-inverse-of : ∀ p → Surjection.to⁻ surjection′ (Surjection.to surjection′ p) ≡ p
+    left-inverse-of : ∀ p → Surjection.from surjection′ (Surjection.to surjection′ p) ≡ p
     left-inverse-of (x , y) = to Σ-≡,≡↔≡
       ( _≃_.left-inverse-of I≃J x
       , (≡.subst A (_≃_.left-inverse-of I≃J x)

src/Data/Product/Function/Dependent/Setoid.agda

@@ -94,34 +94,37 @@ module _ where
     (function (⇔⇒⟶ I⇔J) A⟶B)
     (function (⇔⇒⟵ I⇔J) B⟶A)
 
-  equivalence-↪ :
-    (I↪J : I ↪ J) →
-    (∀ {i} → Equivalence (A atₛ (RightInverse.from I↪J i)) (B atₛ i)) →
-    Equivalence (I ×ₛ A) (J ×ₛ B)
-  equivalence-↪ {A = A} {B = B} I↪J A⇔B =
-    equivalence (RightInverse.equivalence I↪J) A→B (fromFunction A⇔B)
-    where
-    A→B : ∀ {i} → Func (A atₛ i) (B atₛ (RightInverse.to I↪J i))
-    A→B = record
-      { to   = to      A⇔B ∘ cast      A (RightInverse.strictlyInverseʳ I↪J _)
-      ; cong = to-cong A⇔B ∘ cast-cong A (RightInverse.strictlyInverseʳ I↪J _)
-      }
+  module _ (I↪J : I ↪ J) where
 
-  equivalence-↠ :
-    (I↠J : I ↠ J) →
-    (∀ {x} → Equivalence (A atₛ x) (B atₛ (Surjection.to I↠J x))) →
-    Equivalence (I ×ₛ A) (J ×ₛ B)
-  equivalence-↠ {A = A} {B = B} I↠J A⇔B =
-    equivalence (↠⇒⇔ I↠J) B-to B-from
-    where
-    B-to : ∀ {x} → Func (A atₛ x) (B atₛ (Surjection.to I↠J x))
-    B-to = toFunction A⇔B
+    private module ItoJ = RightInverse I↪J
 
-    B-from : ∀ {y} → Func (B atₛ y) (A atₛ (Surjection.to⁻ I↠J y))
-    B-from = record
-      { to   = from      A⇔B ∘ cast      B (Surjection.to∘to⁻ I↠J _)
-      ; cong = from-cong A⇔B ∘ cast-cong B (Surjection.to∘to⁻ I↠J _)
-      }
+    equivalence-↪ : (∀ {i} → Equivalence (A atₛ (ItoJ.from i)) (B atₛ i)) →
+                    Equivalence (I ×ₛ A) (J ×ₛ B)
+    equivalence-↪ {A = A} {B = B} A⇔B =
+      equivalence ItoJ.equivalence A→B (fromFunction A⇔B)
+      where
+      A→B : ∀ {i} → Func (A atₛ i) (B atₛ (ItoJ.to i))
+      A→B = record
+        { to   = to      A⇔B ∘ cast      A (ItoJ.strictlyInverseʳ _)
+        ; cong = to-cong A⇔B ∘ cast-cong A (ItoJ.strictlyInverseʳ _)
+        }
+
+  module _ (I↠J : I ↠ J) where
+
+    private module ItoJ = Surjection I↠J
+
+    equivalence-↠ : (∀ {x} → Equivalence (A atₛ x) (B atₛ (ItoJ.to x))) →
+                    Equivalence (I ×ₛ A) (J ×ₛ B)
+    equivalence-↠ {A = A} {B = B} A⇔B = equivalence (↠⇒⇔ I↠J) B-to B-from
+      where
+      B-to : ∀ {x} → Func (A atₛ x) (B atₛ (ItoJ.to x))
+      B-to = toFunction A⇔B
+
+      B-from : ∀ {y} → Func (B atₛ y) (A atₛ (ItoJ.from y))
+      B-from = record
+        { to   = from      A⇔B ∘ cast      B (ItoJ.strictlyInverseˡ _)
+        ; cong = from-cong A⇔B ∘ cast-cong B (ItoJ.strictlyInverseˡ _)
+        }
 
 ------------------------------------------------------------------------
 -- Injections
@@ -168,12 +171,12 @@ module _ where
     func : Func (I ×ₛ A) (J ×ₛ B)
     func = function (Surjection.function I↠J) (Surjection.function A↠B)
 
-    to⁻′ : Carrier (J ×ₛ B) → Carrier (I ×ₛ A)
-    to⁻′ (j , y) = to⁻ I↠J j , to⁻ A↠B (cast B (Surjection.to∘to⁻ I↠J _) y)
+    from′ : Carrier (J ×ₛ B) → Carrier (I ×ₛ A)
+    from′ (j , y) = from I↠J j , from A↠B (cast B (strictlyInverseˡ I↠J _) y)
 
     strictlySurj : StrictlySurjective (Func.Eq₂._≈_ func) (Func.to func)
-    strictlySurj (j , y) = to⁻′ (j , y) ,
-      to∘to⁻ I↠J j , IndexedSetoid.trans B (to∘to⁻ A↠B _) (cast-eq B (to∘to⁻ I↠J j))
+    strictlySurj (j , y) = from′ (j , y) ,
+      strictlyInverseˡ I↠J j , IndexedSetoid.trans B (strictlyInverseˡ A↠B _) (cast-eq B (strictlyInverseˡ I↠J j))
 
     surj : Surjective (Func.Eq₁._≈_ func) (Func.Eq₂._≈_ func) (Func.to func)
     surj = strictlySurjective⇒surjective (I ×ₛ A) (J ×ₛ B) (Func.cong func) strictlySurj

src/Function/Bundles.agda

@@ -20,16 +20,15 @@
 module Function.Bundles where
 
 open import Function.Base using (_∘_)
+open import Function.Consequences.Propositional
 open import Function.Definitions
 import Function.Structures as FunctionStructures
 open import Level using (Level; _⊔_; suc)
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as ≡
-open import Function.Consequences.Propositional
 open Setoid using (isEquivalence)
 
 private
@@ -113,13 +112,24 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
     open IsSurjection isSurjection public
       using
       ( strictlySurjective
+      ; from
+      ; inverseˡ
+      ; strictlyInverseˡ
       )
 
     to⁻ : B → A
-    to⁻ = proj₁ ∘ surjective
+    to⁻ = from
+    {-# WARNING_ON_USAGE to⁻
+    "Warning: to⁻ was deprecated in v2.3.
+    Please use Function.Structures.IsSurjection.from instead. "
+    #-}
 
-    to∘to⁻ : ∀ x → to (to⁻ x) ≈₂ x
-    to∘to⁻ = proj₂ ∘ strictlySurjective
+    to∘to⁻ : StrictlyInverseˡ _≈₂_ to from
+    to∘to⁻ = strictlyInverseˡ
+    {-# WARNING_ON_USAGE to∘to⁻
+    "Warning: to∘to⁻ was deprecated in v2.3.
+    Please use Function.Structures.IsSurjection.strictlyInverseˡ instead. "
+    #-}
 
 
   record Bijection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
@@ -146,16 +156,24 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
       ; surjective = surjective
       }
 
-    open Injection  injection  public using (isInjection)
-    open Surjection surjection public using (isSurjection; to⁻;  strictlySurjective)
+    open Injection  injection  public
+      using (isInjection)
+    open Surjection surjection public
+      using (isSurjection
+            ; strictlySurjective
+            ; from
+            ; inverseˡ
+            ; strictlyInverseˡ
+            )
 
     isBijection : IsBijection to
     isBijection = record
       { isInjection = isInjection
       ; surjective  = surjective
       }
 
-    open IsBijection isBijection public using (module Eq₁; module Eq₂)
+    open IsBijection isBijection public
+      using (module Eq₁; module Eq₂; inverseʳ; strictlyInverseʳ)
 
 
 ------------------------------------------------------------------------
@@ -220,6 +238,8 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
     open IsLeftInverse isLeftInverse public
       using (module Eq₁; module Eq₂; strictlyInverseˡ; isSurjection)
 
+    open IsSurjection isSurjection public using (surjective)
+
     equivalence : Equivalence
     equivalence = record
       { to-cong   = to-cong
@@ -236,7 +256,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
     surjection = record
       { to = to
       ; cong = to-cong
-      ; surjective = λ y → from y , inverseˡ
+      ; surjective = surjective
       }
 
 
@@ -246,7 +266,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
       to        : A → B
       from      : B → A
       to-cong   : Congruent _≈₁_ _≈₂_ to
-      from-cong : from Preserves _≈₂_ ⟶ _≈₁_
+      from-cong : Congruent _≈₂_ _≈₁_ from
       inverseʳ  : Inverseʳ _≈₁_ _≈₂_ to from
 
     isCongruent : IsCongruent to
@@ -264,14 +284,23 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
       }
 
     open IsRightInverse isRightInverse public
-      using (module Eq₁; module Eq₂; strictlyInverseʳ)
+      using (module Eq₁; module Eq₂; strictlyInverseʳ; isInjection)
+
+    open IsInjection isInjection public using (injective)
 
     equivalence : Equivalence
     equivalence = record
       { to-cong   = to-cong
       ; from-cong = from-cong
       }
 
+    injection : Injection From To
+    injection = record
+      { to = to
+      ; cong = to-cong
+      ; injective = injective
+      }
+
 
   record Inverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field
@@ -370,7 +399,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
   -- function for elements `x₁` and `x₂` are equal if `x₁ ≈ x₂` .
   --
   -- The difference is the `from-cong` law --- generally, the section
-  -- (called `Surjection.to⁻` or `SplitSurjection.from`) of a surjection
+  -- (called `Surjection.from` or `SplitSurjection.from`) of a surjection
   -- need not respect equality, whereas it must in a split surjection.
   --
   -- The two notions coincide when the equivalence relation on `B` is