Added some basic properties of bijections (#1528)

Author: MatthewDaggitt

CHANGELOG.md

@@ -73,6 +73,11 @@ New modules
   Data.Rational.Unnormalised.Show
   ```
 
+* Properties of bijections:
+  ```
+  Function.Properties.Bijection
+  ```
+
 * Various system types and primitives:
   ```
   System.Clock.Primitive
@@ -118,13 +123,23 @@ Other minor additions
   ```
   and their corresponding algebraic substructures.
 
-* In `Data.String.Properties`:
+* Added new proofs in `Data.String.Properties`:
   ```
   ≤-isDecTotalOrder-≈ : IsDecTotalOrder _≈_ _≤_
   ≤-decTotalOrder-≈   :  DecTotalOrder _ _ _
   ```
 
-* In `IO`:
+* Added new proofs in `Function.Construct.Symmetry`:
+  ```
+  bijective     : Bijective ≈₁ ≈₂ f → Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ f⁻¹
+  isBijection   : IsBijection ≈₁ ≈₂ f → Congruent ≈₂ ≈₁ f⁻¹ → IsBijection ≈₂ ≈₁ f⁻¹
+  isBijection-≡ : IsBijection ≈₁ _≡_ f → IsBijection _≡_ ≈₁ f⁻¹
+  bijection     : Bijection R S → Congruent IB.Eq₂._≈_ IB.Eq₁._≈_ f⁻¹ → Bijection S R
+  bijection-≡   : Bijection R (setoid B) → Bijection (setoid B) R
+  sym-⤖        : A ⤖ B → B ⤖ A
+  ```
+
+* Added new operations in `IO`:
   ```
   Colist.forM  : Colist A → (A → IO B) → IO (Colist B)
   Colist.forM′ : Colist A → (A → IO B) → IO ⊤
@@ -133,7 +148,7 @@ Other minor additions
   List.forM′ : List A → (A → IO B) → IO ⊤
   ```
 
-* In `IO.Base`:
+* Added new operations in `IO.Base`:
   ```
   lift! : IO A → IO (Lift b A)
   _<$_  : B → IO A → IO B
@@ -148,8 +163,8 @@ Other minor additions
   untilJust : IO (Maybe A) → IO A
   ```
 
-* In `System.Exit`:
+* Added new operations in `System.Exit`:
   ```
   isSuccess : ExitCode → Bool
   isFailure : ExitCode → Bool
-  ```
+  ```

src/Function/Construct/Symmetry.agda

@@ -8,10 +8,11 @@
 
 module Function.Construct.Symmetry where
 
-open import Data.Product using (_,_; swap)
+open import Data.Product using (_,_; swap; proj₁; proj₂)
 open import Function
 open import Level using (Level)
 open import Relation.Binary hiding (_⇔_)
+open import Relation.Binary.PropositionalEquality
 
 private
   variable
@@ -23,6 +24,23 @@ private
 ------------------------------------------------------------------------
 -- Properties
 
+module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B}
+         ((inj , surj) : Bijective ≈₁ ≈₂ f)
+         where
+
+  private
+    f⁻¹      = proj₁ ∘ surj
+    f∘f⁻¹≡id = proj₂ ∘ surj
+
+  injective : Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₁ ≈₂ f → Injective ≈₂ ≈₁ f⁻¹
+  injective sym trans cong gx≈gy = trans (trans (sym (f∘f⁻¹≡id _)) (cong gx≈gy)) (f∘f⁻¹≡id _)
+
+  surjective : Surjective ≈₂ ≈₁ f⁻¹
+  surjective x = f x , inj (proj₂ (surj (f x)))
+
+  bijective : Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ f⁻¹
+  bijective sym trans cong = injective sym trans cong , surjective
+
 module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂)
          (f : A → B) {f⁻¹ : B → A}
          where
@@ -39,85 +57,136 @@ module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂)
 ------------------------------------------------------------------------
 -- Structures
 
+module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂}
+         {f : A → B} (isBij : IsBijection ≈₁ ≈₂ f)
+         where
+
+  private
+    module IB = IsBijection isBij
+    f⁻¹       = proj₁ ∘ IB.surjective
+
+  -- We can only flip a bijection if the witness produced by the
+  -- surjection proof respects the equality on the codomain.
+  isBijection : Congruent ≈₂ ≈₁ f⁻¹ → IsBijection ≈₂ ≈₁ f⁻¹
+  isBijection f⁻¹-cong = record
+    { isInjection = record
+      { isCongruent = record
+        { cong           = f⁻¹-cong
+        ; isEquivalence₁ = IB.Eq₂.isEquivalence
+        ; isEquivalence₂ = IB.Eq₁.isEquivalence
+        }
+      ; injective = injective IB.bijective IB.Eq₂.sym IB.Eq₂.trans IB.cong
+      }
+    ; surjective = surjective {≈₂ = ≈₂} IB.bijective
+    }
+
+module _ {≈₁ : Rel A ℓ₁} {f : A → B} (isBij : IsBijection ≈₁ _≡_ f) where
+
+  -- We can always flip a bijection if using the equality over the
+  -- codomain is propositional equality.
+  isBijection-≡ : IsBijection _≡_ ≈₁ _
+  isBijection-≡ = isBijection isBij (IB.Eq₁.reflexive ∘ cong _)
+    where module IB = IsBijection isBij
+
 module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂}
          {f : A → B} {f⁻¹ : B → A}
          where
 
   isCongruent : IsCongruent ≈₁ ≈₂ f → Congruent ≈₂ ≈₁ f⁻¹ → IsCongruent ≈₂ ≈₁ f⁻¹
   isCongruent ic cg = record
-    { cong = cg
+    { cong           = cg
     ; isEquivalence₁ = IC.isEquivalence₂
     ; isEquivalence₂ = IC.isEquivalence₁
-    }
-    where module IC = IsCongruent ic
+    } where module IC = IsCongruent ic
 
   isLeftInverse : IsRightInverse ≈₁ ≈₂ f f⁻¹ → IsLeftInverse ≈₂ ≈₁ f⁻¹ f
   isLeftInverse inv = record
     { isCongruent = isCongruent F.isCongruent F.cong₂
-    ; cong₂ = F.cong₁
-    ; inverseˡ = inverseˡ ≈₁ ≈₂ f {f⁻¹} F.inverseʳ
-    }
-    where module F = IsRightInverse inv
+    ; cong₂       = F.cong₁
+    ; inverseˡ    = inverseˡ ≈₁ ≈₂ f {f⁻¹} F.inverseʳ
+    } where module F = IsRightInverse inv
 
   isRightInverse : IsLeftInverse ≈₁ ≈₂ f f⁻¹ → IsRightInverse ≈₂ ≈₁ f⁻¹ f
   isRightInverse inv = record
     { isCongruent = isCongruent F.isCongruent F.cong₂
-    ; cong₂ = F.cong₁
-    ; inverseʳ = inverseʳ ≈₁ ≈₂ f {f⁻¹} F.inverseˡ
-    }
-    where module F = IsLeftInverse inv
+    ; cong₂       = F.cong₁
+    ; inverseʳ    = inverseʳ ≈₁ ≈₂ f {f⁻¹} F.inverseˡ
+    } where module F = IsLeftInverse inv
 
   isInverse : IsInverse ≈₁ ≈₂ f f⁻¹ → IsInverse ≈₂ ≈₁ f⁻¹ f
   isInverse f-inv = record
     { isLeftInverse = isLeftInverse F.isRightInverse
-    ; inverseʳ = inverseʳ ≈₁ ≈₂ f F.inverseˡ
-    }
-    where module F = IsInverse f-inv
+    ; inverseʳ      = inverseʳ ≈₁ ≈₂ f F.inverseˡ
+    } where module F = IsInverse f-inv
 
 ------------------------------------------------------------------------
 -- Setoid bundles
 
+module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} (bij : Bijection R S) where
+
+  private
+    module IB = Bijection bij
+    f⁻¹       = proj₁ ∘ IB.surjective
+
+  -- We can only flip a bijection if the witness produced by the
+  -- surjection proof respects the equality on the codomain.
+  bijection : Congruent IB.Eq₂._≈_ IB.Eq₁._≈_ f⁻¹ → Bijection S R
+  bijection cong = record
+    { f         = f⁻¹
+    ; cong      = cong
+    ; bijective = bijective IB.bijective IB.Eq₂.sym IB.Eq₂.trans IB.cong
+    }
+
+-- We can always flip a bijection if using the equality over the
+-- codomain is propositional equality.
+bijection-≡ : {R : Setoid a ℓ₁} {B : Set b} →
+              Bijection R (setoid B) → Bijection (setoid B) R
+bijection-≡ bij = bijection bij (B.Eq₁.reflexive ∘ cong _)
+ where module B = Bijection bij
+
 module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} where
 
   equivalence : Equivalence R S → Equivalence S R
   equivalence equiv = record
-    { f = E.g
-    ; g = E.f
+    { f     = E.g
+    ; g     = E.f
     ; cong₁ = E.cong₂
     ; cong₂ = E.cong₁
-    }
-    where module E = Equivalence equiv
+    } where module E = Equivalence equiv
 
   rightInverse : LeftInverse R S → RightInverse S R
   rightInverse left = record
-    { f = L.g
-    ; g = L.f
-    ; cong₁ = L.cong₂
-    ; cong₂ = L.cong₁
+    { f        = L.g
+    ; g        = L.f
+    ; cong₁    = L.cong₂
+    ; cong₂    = L.cong₁
     ; inverseʳ = L.inverseˡ
     } where module L = LeftInverse left
 
   leftInverse : RightInverse R S → LeftInverse S R
   leftInverse right = record
-    { f = R.g
-    ; g = R.f
+    { f     = R.g
+    ; g     = R.f
     ; cong₁ = R.cong₂
     ; cong₂ = R.cong₁
     ; inverseˡ = R.inverseʳ
     } where module R = RightInverse right
 
   inverse : Inverse R S → Inverse S R
   inverse inv = record
-    { f = I.f⁻¹
-    ; f⁻¹ = I.f
-    ; cong₁ = I.cong₂
-    ; cong₂ = I.cong₁
+    { f       = I.f⁻¹
+    ; f⁻¹     = I.f
+    ; cong₁   = I.cong₂
+    ; cong₂   = I.cong₁
     ; inverse = swap I.inverse
     } where module I = Inverse inv
 
 ------------------------------------------------------------------------
 -- Propositional bundles
 
+sym-⤖ : A ⤖ B → B ⤖ A
+sym-⤖ b = bijection b (cong _)
+
 sym-⇔ : A ⇔ B → B ⇔ A
 sym-⇔ = equivalence
 

src/Function/Properties/Bijection.agda

@@ -0,0 +1,49 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some basic properties of bijections. This file is designed to be
+-- imported qualified.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Function.Properties.Bijection where
+
+open import Function.Bundles using (Bijection; _⤖_)
+open import Level using (Level)
+open import Relation.Binary
+import Relation.Binary.PropositionalEquality as P
+
+import Function.Construct.Identity as Identity
+import Function.Construct.Symmetry as Symmetry
+import Function.Construct.Composition as Composition
+
+private
+  variable
+    a b c ℓ ℓ₁ ℓ₂ ℓ₃ : Level
+    A B : Set a
+    T S : Setoid a ℓ
+
+------------------------------------------------------------------------
+-- Setoid properties
+
+refl : Reflexive (Bijection {a} {ℓ})
+refl = Identity.bijection _
+
+-- Can't prove full symmetry as we have no proof that the witness
+-- produced by the surjection proof preserves equality
+sym-≡ : Bijection S (P.setoid B) → Bijection (P.setoid B) S
+sym-≡ = Symmetry.bijection-≡
+
+trans : Trans (Bijection {a} {ℓ₁} {b} {ℓ₂}) (Bijection {b} {ℓ₂} {c} {ℓ₃}) Bijection
+trans = Composition.bijection
+
+------------------------------------------------------------------------
+-- Propositional properties
+
+⤖-isEquivalence : IsEquivalence {ℓ = ℓ} _⤖_
+⤖-isEquivalence = record
+  { refl  = refl
+  ; sym   = sym-≡
+  ; trans = trans
+  }

src/Function/Properties/Equivalence.agda

@@ -1,8 +1,8 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- An Equivalence (on functions) is an Equivalence relation
---   This file is meant to be imported qualified.
+-- Some basic properties of equivalences. This file is designed to be
+-- imported qualified.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
@@ -20,12 +20,12 @@ import Function.Construct.Composition as Composition
 
 private
   variable
-    a b ℓ₁ ℓ₂ : Level
+    a ℓ : Level
 
 ------------------------------------------------------------------------
 -- Setoid bundles
 
-isEquivalence : IsEquivalence (Equivalence {a} {b})
+isEquivalence : IsEquivalence (Equivalence {a} {ℓ})
 isEquivalence = record
   { refl = λ {x} → Identity.equivalence x
   ; sym = Symmetry.equivalence
@@ -35,7 +35,7 @@ isEquivalence = record
 ------------------------------------------------------------------------
 -- Propositional bundles
 
-⇔-isEquivalence : IsEquivalence {ℓ = ℓ₁} _⇔_
+⇔-isEquivalence : IsEquivalence {ℓ = ℓ} _⇔_
 ⇔-isEquivalence = record
   { refl = λ {x} → Identity.equivalence (setoid x)
   ; sym = Symmetry.equivalence

src/Function/Properties/Inverse.agda

@@ -12,33 +12,33 @@ module Function.Properties.Inverse where
 open import Function.Bundles using (Inverse; _↔_)
 open import Level using (Level)
 open import Relation.Binary using (Setoid; IsEquivalence)
-open import Relation.Binary.PropositionalEquality using (setoid)
+import Relation.Binary.PropositionalEquality as P
 
 import Function.Construct.Identity as Identity
 import Function.Construct.Symmetry as Symmetry
 import Function.Construct.Composition as Composition
 
 private
   variable
-    a b ℓ₁ ℓ₂ : Level
+    a ℓ : Level
 
 ------------------------------------------------------------------------
 -- Setoid bundles
 
-isEquivalence : IsEquivalence (Inverse {a} {b})
+isEquivalence : IsEquivalence (Inverse {a} {ℓ})
 isEquivalence = record
-  { refl = λ {x} → Identity.inverse x
-  ; sym = Symmetry.inverse
+  { refl  = λ {x} → Identity.inverse x
+  ; sym   = Symmetry.inverse
   ; trans = Composition.inverse
   }
 
 ------------------------------------------------------------------------
 -- Propositional bundles
 
 -- need to η-expand for everything to line up properly
-↔-isEquivalence : IsEquivalence {ℓ = ℓ₁} _↔_
+↔-isEquivalence : IsEquivalence {ℓ = ℓ} _↔_
 ↔-isEquivalence = record
-  { refl = λ {x} → Identity.inverse (setoid x)
-  ; sym = Symmetry.inverse
+  { refl  = λ {x} → Identity.inverse (P.setoid x)
+  ; sym   = Symmetry.inverse
   ; trans = Composition.inverse
   }