Add Function.Consequences.Setoid

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`
 
@@ -2012,6 +2012,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 (_⊔_)
 
 ------------------------------------------------------------------------