Add Function.Consequences.Setoid (#2191)

* Add Function.Consequences.Setoid

* Fix comment

* Fix re-export bug

* Finally fixed bug I hope

* Removed rogue comment

* More tidying up

Author: MatthewDaggitt

CHANGELOG.md

@@ -752,7 +752,7 @@ Non-backwards compatible changes
          of these under the names `strictlySurjective`, `strictlyInverseˡ` and
          `strictlyInverseʳ`,
    - Conversion functions have been added in both directions to
-         `Function.Consequences(.Propositional)`.
+         `Function.Consequences(.Propositional/Setoid)`.
 
 ### New `Function.Strict`
 
@@ -2028,6 +2028,8 @@ New modules
 * Properties of various types of functions:
   ```
   Function.Consequences
+  Function.Consequences.Setoid
+  Function.Consequences.Propositional
   Function.Properties.Bijection
   Function.Properties.RightInverse
   Function.Properties.Surjection

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

@@ -15,7 +15,7 @@ open import Data.Product.Base using (map; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.Dependent as Σ
 open import Level using (Level)
 open import Function
-open import Function.Consequences
+open import Function.Consequences.Setoid
 open import Function.Properties.Injection using (mkInjection)
 open import Function.Properties.Surjection using (mkSurjection; ↠⇒⇔)
 open import Function.Properties.Equivalence using (mkEquivalence; ⇔⇒⟶; ⇔⇒⟵)
@@ -176,7 +176,7 @@ module _ where
       to∘to⁻ I↠J j , IndexedSetoid.trans B (to∘to⁻ A↠B _) (cast-eq B (to∘to⁻ I↠J j))
 
     surj : Surjective (Func.Eq₁._≈_ func) (Func.Eq₂._≈_ func) (Func.to func)
-    surj = strictlySurjective⇒surjective (trans (J ×ₛ B)) (Func.cong func) strictlySurj
+    surj = strictlySurjective⇒surjective (I ×ₛ A) (J ×ₛ B) (Func.cong func) strictlySurj
 
 ------------------------------------------------------------------------
 -- LeftInverse
@@ -199,7 +199,7 @@ module _ where
     strictlyInvʳ (i , x) = strictlyInverseʳ I↪J i , IndexedSetoid.trans A (strictlyInverseʳ A↪B _) (cast-eq A (strictlyInverseʳ I↪J i))
 
     invʳ : Inverseʳ (_≈_ (I ×ₛ A)) (_≈_ (J ×ₛ B)) (Equivalence.to equiv) (Equivalence.from equiv)
-    invʳ = strictlyInverseʳ⇒inverseʳ {f⁻¹ = Equivalence.from equiv} (trans (I ×ₛ A)) (Equivalence.from-cong equiv) strictlyInvʳ
+    invʳ = strictlyInverseʳ⇒inverseʳ (I ×ₛ A) (J ×ₛ B) (Equivalence.from-cong equiv) strictlyInvʳ
 
 
 ------------------------------------------------------------------------
@@ -238,7 +238,7 @@ module _ where
           (cast-eq B (strictlyInverseˡ I↔J i))
 
     invˡ : Inverseˡ (_≈_ (I ×ₛ A)) (_≈_ (J ×ₛ B)) to′ from′
-    invˡ = strictlyInverseˡ⇒inverseˡ {≈₁ = _≈_ (I ×ₛ A)} {f⁻¹ = from′} (trans (J ×ₛ B)) to′-cong strictlyInvˡ
+    invˡ = strictlyInverseˡ⇒inverseˡ (I ×ₛ A) (J ×ₛ B) to′-cong strictlyInvˡ
 
     lem : ∀ {i j} → i ≡ j → ∀ {x : IndexedSetoid.Carrier B (to I↔J i)} {y : IndexedSetoid.Carrier B (to I↔J j)} →
           IndexedSetoid._≈_ B x y →
@@ -250,5 +250,5 @@ module _ where
       IndexedSetoid.trans A (lem (strictlyInverseʳ I↔J _) (cast-eq B (strictlyInverseˡ I↔J _))) (strictlyInverseʳ A↔B _)
 
     invʳ : Inverseʳ (_≈_ (I ×ₛ A)) (_≈_ (J ×ₛ B)) to′ from′
-    invʳ = strictlyInverseʳ⇒inverseʳ {f⁻¹ = from′} (trans (I ×ₛ A)) from′-cong strictlyInvʳ
+    invʳ = strictlyInverseʳ⇒inverseʳ (I ×ₛ A) (J ×ₛ B) from′-cong strictlyInvʳ
 

src/Function/Consequences.agda

@@ -28,9 +28,9 @@ private
 ------------------------------------------------------------------------
 -- Injective
 
-contraInjective : Injective ≈₁ ≈₂ f →
+contraInjective : ∀ (≈₂ : Rel B ℓ₂) → Injective ≈₁ ≈₂ f →
                   ∀ {x y} → ¬ (≈₁ x y) → ¬ (≈₂ (f x) (f y))
-contraInjective inj p = contraposition inj p
+contraInjective _ inj p = contraposition inj p
 
 ------------------------------------------------------------------------
 -- Inverseˡ

src/Function/Consequences/Propositional.agda

@@ -7,85 +7,47 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-module Function.Consequences.Propositional where
+module Function.Consequences.Propositional
+  {a b} {A : Set a} {B : Set b}
+  where
 
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; cong)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (setoid)
 open import Function.Definitions
-open import Level
 open import Relation.Nullary.Negation.Core using (contraposition)
-open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; _≢_; refl; sym; trans; cong)
 
-import Function.Consequences as C
-
-private
-  variable
-    a b ℓ₁ ℓ₂ : Level
-    A B : Set a
-    f f⁻¹ : A → B
-
-------------------------------------------------------------------------
--- Injective
-
-contraInjective : Injective _≡_ _≡_ f →
-                  ∀ {x y} → x ≢ y → f x ≢ f y
-contraInjective inj p = contraposition inj p
-
-------------------------------------------------------------------------
--- Inverseˡ
-
-inverseˡ⇒surjective : Inverseˡ _≡_ _≡_ f f⁻¹ → Surjective _≡_ _≡_ f
-inverseˡ⇒surjective = C.inverseˡ⇒surjective _≡_
-
-------------------------------------------------------------------------
--- Inverseʳ
-
-inverseʳ⇒injective : ∀ f →
-                     Inverseʳ _≡_ _≡_ f f⁻¹ →
-                     Injective _≡_ _≡_ f
-inverseʳ⇒injective f = C.inverseʳ⇒injective _≡_ f refl sym trans
+import Function.Consequences.Setoid (setoid A) (setoid B) as Setoid
 
 ------------------------------------------------------------------------
--- Inverseᵇ
+-- Re-export setoid properties
 
-inverseᵇ⇒bijective : Inverseᵇ _≡_ _≡_ f f⁻¹ → Bijective _≡_ _≡_ f
-inverseᵇ⇒bijective = C.inverseᵇ⇒bijective _≡_ refl sym trans
+open Setoid public
+  hiding
+  ( strictlySurjective⇒surjective
+  ; strictlyInverseˡ⇒inverseˡ
+  ; strictlyInverseʳ⇒inverseʳ
+  )
 
 ------------------------------------------------------------------------
--- StrictlySurjective
+-- Properties that rely on congruence
 
-surjective⇒strictlySurjective : Surjective _≡_ _≡_ f →
-                                 StrictlySurjective _≡_ f
-surjective⇒strictlySurjective =
-  C.surjective⇒strictlySurjective _≡_ refl
+private
+  variable
+    f : A → B
+    f⁻¹ : B → A
 
 strictlySurjective⇒surjective : StrictlySurjective _≡_ f →
                                  Surjective _≡_ _≡_ f
 strictlySurjective⇒surjective =
-  C.strictlySurjective⇒surjective trans (cong _)
-
-------------------------------------------------------------------------
--- StrictlyInverseˡ
-
-inverseˡ⇒strictlyInverseˡ : Inverseˡ _≡_ _≡_ f f⁻¹ →
-                            StrictlyInverseˡ _≡_ f f⁻¹
-inverseˡ⇒strictlyInverseˡ =
-  C.inverseˡ⇒strictlyInverseˡ _≡_ _≡_ refl
+ Setoid.strictlySurjective⇒surjective (cong _)
 
-strictlyInverseˡ⇒inverseˡ : ∀ f →
-                            StrictlyInverseˡ _≡_ f f⁻¹ →
+strictlyInverseˡ⇒inverseˡ : ∀ f → StrictlyInverseˡ _≡_ f f⁻¹ →
                             Inverseˡ _≡_ _≡_ f f⁻¹
 strictlyInverseˡ⇒inverseˡ f =
-  C.strictlyInverseˡ⇒inverseˡ trans (cong f)
-
-------------------------------------------------------------------------
--- StrictlyInverseʳ
-
-inverseʳ⇒strictlyInverseʳ : Inverseʳ _≡_ _≡_ f f⁻¹ →
-                            StrictlyInverseʳ _≡_ f f⁻¹
-inverseʳ⇒strictlyInverseʳ = C.inverseʳ⇒strictlyInverseʳ _≡_ _≡_ refl
+  Setoid.strictlyInverseˡ⇒inverseˡ (cong _)
 
-strictlyInverseʳ⇒inverseʳ : ∀ f →
-                            StrictlyInverseʳ _≡_ f f⁻¹ →
+strictlyInverseʳ⇒inverseʳ : ∀ f → StrictlyInverseʳ _≡_ f f⁻¹ →
                             Inverseʳ _≡_ _≡_ f f⁻¹
-strictlyInverseʳ⇒inverseʳ {f⁻¹ = f⁻¹} _ =
-  C.strictlyInverseʳ⇒inverseʳ trans (cong f⁻¹)
+strictlyInverseʳ⇒inverseʳ f =
+  Setoid.strictlyInverseʳ⇒inverseʳ (cong _)

src/Function/Consequences/Setoid.agda

@@ -0,0 +1,92 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Relationships between properties of functions where the equality
+-- over both the domain and codomain are assumed to be setoids.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Bundles using (Setoid)
+
+module Function.Consequences.Setoid
+  {a b ℓ₁ ℓ₂}
+  (S : Setoid a ℓ₁)
+  (T : Setoid b ℓ₂)
+  where
+
+open import Function.Definitions
+open import Relation.Nullary.Negation.Core
+
+import Function.Consequences as C
+
+private
+  open module S = Setoid S using () renaming (Carrier to A; _≈_ to ≈₁)
+  open module T = Setoid T using () renaming (Carrier to B; _≈_ to ≈₂)
+
+  variable
+    f : A → B
+    f⁻¹ : B → A
+
+------------------------------------------------------------------------
+-- Injective
+
+contraInjective : Injective ≈₁ ≈₂ f →
+                  ∀ {x y} → ¬ (≈₁ x y) → ¬ (≈₂ (f x) (f y))
+contraInjective = C.contraInjective ≈₂
+
+------------------------------------------------------------------------
+-- Inverseˡ
+
+inverseˡ⇒surjective : Inverseˡ ≈₁ ≈₂ f f⁻¹ → Surjective ≈₁ ≈₂ f
+inverseˡ⇒surjective = C.inverseˡ⇒surjective ≈₂
+
+------------------------------------------------------------------------
+-- Inverseʳ
+
+inverseʳ⇒injective : ∀ f → Inverseʳ ≈₁ ≈₂ f f⁻¹ → Injective ≈₁ ≈₂ f
+inverseʳ⇒injective f = C.inverseʳ⇒injective ≈₂ f T.refl S.sym S.trans
+
+------------------------------------------------------------------------
+-- Inverseᵇ
+
+inverseᵇ⇒bijective : Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Bijective ≈₁ ≈₂ f
+inverseᵇ⇒bijective = C.inverseᵇ⇒bijective ≈₂ T.refl S.sym S.trans
+
+------------------------------------------------------------------------
+-- StrictlySurjective
+
+surjective⇒strictlySurjective : Surjective ≈₁ ≈₂ f →
+                                 StrictlySurjective ≈₂ f
+surjective⇒strictlySurjective =
+  C.surjective⇒strictlySurjective ≈₂ S.refl
+
+strictlySurjective⇒surjective : Congruent ≈₁ ≈₂ f →
+                                 StrictlySurjective ≈₂ f →
+                                 Surjective ≈₁ ≈₂ f
+strictlySurjective⇒surjective =
+  C.strictlySurjective⇒surjective T.trans
+
+------------------------------------------------------------------------
+-- StrictlyInverseˡ
+
+inverseˡ⇒strictlyInverseˡ : Inverseˡ ≈₁ ≈₂ f f⁻¹ →
+                            StrictlyInverseˡ ≈₂ f f⁻¹
+inverseˡ⇒strictlyInverseˡ = C.inverseˡ⇒strictlyInverseˡ ≈₁ ≈₂ S.refl
+
+strictlyInverseˡ⇒inverseˡ : Congruent ≈₁ ≈₂ f →
+                            StrictlyInverseˡ ≈₂ f f⁻¹ →
+                            Inverseˡ ≈₁ ≈₂ f f⁻¹
+strictlyInverseˡ⇒inverseˡ = C.strictlyInverseˡ⇒inverseˡ T.trans
+
+------------------------------------------------------------------------
+-- StrictlyInverseʳ
+
+inverseʳ⇒strictlyInverseʳ : Inverseʳ ≈₁ ≈₂ f f⁻¹ →
+                            StrictlyInverseʳ ≈₁ f f⁻¹
+inverseʳ⇒strictlyInverseʳ = C.inverseʳ⇒strictlyInverseʳ ≈₁ ≈₂ T.refl
+
+strictlyInverseʳ⇒inverseʳ : Congruent ≈₂ ≈₁ f⁻¹ →
+                            StrictlyInverseʳ ≈₁ f f⁻¹ →
+                            Inverseʳ ≈₁ ≈₂ f f⁻¹
+strictlyInverseʳ⇒inverseʳ = C.strictlyInverseʳ⇒inverseʳ S.trans

src/Function/Properties/Inverse.agda

@@ -19,7 +19,7 @@ open import Relation.Binary.Structures using (IsEquivalence)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as P
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
-open import Function.Consequences
+import Function.Consequences.Setoid as Consequences
 
 import Function.Construct.Identity as Identity
 import Function.Construct.Symmetry as Symmetry
@@ -77,25 +77,25 @@ fromFunction I = record { to = from ; cong = from-cong }
   where open Inverse I
 
 Inverse⇒Injection : Inverse S T → Injection S T
-Inverse⇒Injection I = record
+Inverse⇒Injection {S = S} {T = T} I = record
   { to = to
   ; cong = to-cong
-  ; injective = inverseʳ⇒injective Eq₂._≈_ to Eq₂.refl Eq₁.sym Eq₁.trans inverseʳ
-  } where open Inverse I
+  ; injective = inverseʳ⇒injective to inverseʳ
+  } where open Inverse I; open Consequences S T
 
 Inverse⇒Surjection : Inverse S T → Surjection S T
 Inverse⇒Surjection {S = S} {T = T} I = record
   { to = to
   ; cong = to-cong
-  ; surjective = inverseˡ⇒surjective (_≈_ T) inverseˡ
-  } where open Inverse I; open Setoid
+  ; surjective = inverseˡ⇒surjective inverseˡ
+  } where open Inverse I; open Consequences S T
 
 Inverse⇒Bijection : Inverse S T → Bijection S T
-Inverse⇒Bijection I = record
+Inverse⇒Bijection {S = S} {T = T} I = record
   { to        = to
   ; cong      = to-cong
-  ; bijective = inverseᵇ⇒bijective Eq₂._≈_ Eq₂.refl Eq₁.sym Eq₁.trans inverse
-  } where open Inverse I
+  ; bijective = inverseᵇ⇒bijective inverse
+  } where open Inverse I; open Consequences S T
 
 Inverse⇒Equivalence : Inverse S T → Equivalence S T
 Inverse⇒Equivalence I = record

src/Function/Structures.agda

@@ -20,7 +20,6 @@ module Function.Structures {a b ℓ₁ ℓ₂}
 open import Data.Product.Base as Product using (∃; _×_; _,_)
 open import Function.Base
 open import Function.Definitions
-open import Function.Consequences
 open import Level using (_⊔_)
 
 ------------------------------------------------------------------------