refactor: v3.0 version of agda#2569

Author: jamesmckinna

src/Function/Bundles.agda

@@ -20,16 +20,16 @@
 module Function.Bundles where
 
 open import Function.Base using (_∘_)
+open import Function.Consequences.Propositional
+  using (strictlySurjective⇒surjective; strictlyInverseˡ⇒inverseˡ; strictlyInverseʳ⇒inverseʳ)
 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 +113,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 +157,27 @@ 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ʳ
+            ; from-cong; from-injective; from-surjective; from-bijective
+            )
 
 
 ------------------------------------------------------------------------
@@ -220,6 +242,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 +260,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 +270,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 +288,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 +403,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

src/Function/Consequences.agda

@@ -11,6 +11,7 @@
 module Function.Consequences where
 
 open import Data.Product.Base as Product
+open import Function.Base using (_∘_)
 open import Function.Definitions
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
@@ -23,22 +24,23 @@ private
     a b ℓ₁ ℓ₂ : Level
     A B : Set a
     ≈₁ ≈₂ : Rel A ℓ₁
-    f f⁻¹ : A → B
+    f : A → B
+    f⁻¹ : B → A
 
 ------------------------------------------------------------------------
 -- Injective
 
 contraInjective : ∀ (≈₂ : Rel B ℓ₂) → Injective ≈₁ ≈₂ f →
                   ∀ {x y} → ¬ (≈₁ x y) → ¬ (≈₂ (f x) (f y))
-contraInjective _ inj p = contraposition inj p
+contraInjective _ inj = contraposition inj
 
 ------------------------------------------------------------------------
 -- Inverseˡ
 
 inverseˡ⇒surjective : ∀ (≈₂ : Rel B ℓ₂) →
                       Inverseˡ ≈₁ ≈₂ f f⁻¹ →
                       Surjective ≈₁ ≈₂ f
-inverseˡ⇒surjective ≈₂ invˡ y = (_ , invˡ)
+inverseˡ⇒surjective ≈₂ invˡ _ = (_ , invˡ)
 
 ------------------------------------------------------------------------
 -- Inverseʳ
@@ -49,8 +51,7 @@ inverseʳ⇒injective : ∀ (≈₂ : Rel B ℓ₂) f →
                      Transitive ≈₁ →
                      Inverseʳ ≈₁ ≈₂ f f⁻¹ →
                      Injective ≈₁ ≈₂ f
-inverseʳ⇒injective ≈₂ f refl sym trans invʳ {x} {y} fx≈fy =
-  trans (sym (invʳ refl)) (invʳ fx≈fy)
+inverseʳ⇒injective ≈₂ f refl sym trans invʳ = trans (sym (invʳ refl)) ∘ invʳ
 
 ------------------------------------------------------------------------
 -- Inverseᵇ
@@ -71,8 +72,7 @@ surjective⇒strictlySurjective : ∀ (≈₂ : Rel B ℓ₂) →
                                  Reflexive ≈₁ →
                                  Surjective ≈₁ ≈₂ f →
                                  StrictlySurjective ≈₂ f
-surjective⇒strictlySurjective _ refl surj x =
-  Product.map₂ (λ v → v refl) (surj x)
+surjective⇒strictlySurjective _ refl surj = Product.map₂ (λ v → v refl) ∘ surj
 
 strictlySurjective⇒surjective : Transitive ≈₂ →
                                  Congruent ≈₁ ≈₂ f →
@@ -104,11 +104,13 @@ inverseʳ⇒strictlyInverseʳ : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ
                             Reflexive ≈₂ →
                             Inverseʳ ≈₁ ≈₂ f f⁻¹ →
                             StrictlyInverseʳ ≈₁ f f⁻¹
-inverseʳ⇒strictlyInverseʳ _ _ refl sinv x = sinv refl
+inverseʳ⇒strictlyInverseʳ  {f = f} {f⁻¹ = f⁻¹} ≈₁ ≈₂ =
+  inverseˡ⇒strictlyInverseˡ {f = f⁻¹} {f⁻¹ = f} ≈₂ ≈₁
 
 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ʳ⇒inverseʳ {≈₁ = ≈₁} {≈₂ = ≈₂} {f⁻¹ = f⁻¹} {f = f} =
+  strictlyInverseˡ⇒inverseˡ {≈₂ = ≈₁} {≈₁ = ≈₂} {f = f⁻¹} {f⁻¹ = f}
+

src/Function/Consequences/Propositional.agda

@@ -11,18 +11,16 @@ module Function.Consequences.Propositional
   {a b} {A : Set a} {B : Set b}
   where
 
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; cong)
+open import Data.Product.Base using (_,_)
+open import Function.Definitions
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Binary.PropositionalEquality.Properties
   using (setoid)
-open import Function.Definitions
-open import Relation.Nullary.Negation.Core using (contraposition)
-
-import Function.Consequences.Setoid (setoid A) (setoid B) as Setoid
 
 ------------------------------------------------------------------------
 -- Re-export setoid properties
 
-open Setoid public
+open import Function.Consequences.Setoid (setoid A) (setoid B) public
   hiding
   ( strictlySurjective⇒surjective
   ; strictlyInverseˡ⇒inverseˡ
@@ -39,15 +37,14 @@ private
 
 strictlySurjective⇒surjective : StrictlySurjective _≡_ f →
                                  Surjective _≡_ _≡_ f
-strictlySurjective⇒surjective =
- Setoid.strictlySurjective⇒surjective (cong _)
+strictlySurjective⇒surjective surj y =
+  let x , fx≡y = surj y in x , λ where refl → fx≡y
 
 strictlyInverseˡ⇒inverseˡ : ∀ f → StrictlyInverseˡ _≡_ f f⁻¹ →
                             Inverseˡ _≡_ _≡_ f f⁻¹
-strictlyInverseˡ⇒inverseˡ f =
-  Setoid.strictlyInverseˡ⇒inverseˡ (cong _)
+strictlyInverseˡ⇒inverseˡ _ inv refl = inv _
 
 strictlyInverseʳ⇒inverseʳ : ∀ f → StrictlyInverseʳ _≡_ f f⁻¹ →
                             Inverseʳ _≡_ _≡_ f f⁻¹
-strictlyInverseʳ⇒inverseʳ f =
-  Setoid.strictlyInverseʳ⇒inverseʳ (cong _)
+strictlyInverseʳ⇒inverseʳ _ inv refl = inv _
+