diff --git a/CHANGELOG.md b/CHANGELOG.md index 479eb395bc..7cda9fde57 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda index f290c7341b..22cb950626 100644 --- a/src/Data/Product/Function/Dependent/Setoid.agda +++ b/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ʳ diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda index 60606cc673..2fda92224e 100644 --- a/src/Function/Consequences.agda +++ b/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ˡ diff --git a/src/Function/Consequences/Propositional.agda b/src/Function/Consequences/Propositional.agda index d6067a7702..a2558a9c48 100644 --- a/src/Function/Consequences/Propositional.agda +++ b/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 _) diff --git a/src/Function/Consequences/Setoid.agda b/src/Function/Consequences/Setoid.agda new file mode 100644 index 0000000000..d2c3b948d9 --- /dev/null +++ b/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 diff --git a/src/Function/Properties/Inverse.agda b/src/Function/Properties/Inverse.agda index 87ce778fec..5ade85d843 100644 --- a/src/Function/Properties/Inverse.agda +++ b/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 diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index baf33dddf0..ae34203fe0 100644 --- a/src/Function/Structures.agda +++ b/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 (_⊔_) ------------------------------------------------------------------------