From 743f873c2cec9c220a3edc0e48746b020055bf24 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Thu, 2 Nov 2023 12:11:31 +0900 Subject: [PATCH 1/6] Add Function.Consequences.Setoid --- CHANGELOG.md | 3 +- .../Product/Function/Dependent/Setoid.agda | 10 +-- src/Function/Consequences/Propositional.agda | 84 +++++------------ src/Function/Consequences/Setoid.agda | 90 +++++++++++++++++++ src/Function/Properties/Inverse.agda | 18 ++-- src/Function/Structures.agda | 1 - 6 files changed, 129 insertions(+), 77 deletions(-) create mode 100644 src/Function/Consequences/Setoid.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 479eb395bc..b7d88b83d0 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,7 @@ New modules * Properties of various types of functions: ``` Function.Consequences + Function.Consequences.Setoid 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..1779a99915 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ʳ -- (Equivalence.from equiv) ------------------------------------------------------------------------ @@ -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/Propositional.agda b/src/Function/Consequences/Propositional.agda index d6067a7702..1bdc31410e 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 +import Function.Consequences.Setoid (setoid A) (setoid B) as SetoidConsequences 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 - + f : A → B + f⁻¹ : B → A + ------------------------------------------------------------------------ --- Inverseˡ +-- Re-export setoid properties -inverseˡ⇒surjective : Inverseˡ _≡_ _≡_ f f⁻¹ → Surjective _≡_ _≡_ f -inverseˡ⇒surjective = C.inverseˡ⇒surjective _≡_ +open SetoidConsequences public + hiding + ( strictlySurjective⇒surjective + ; strictlyInverseˡ⇒inverseˡ + ; strictlyInverseʳ⇒inverseʳ + ) ------------------------------------------------------------------------ --- Inverseʳ - -inverseʳ⇒injective : ∀ f → - Inverseʳ _≡_ _≡_ f f⁻¹ → - Injective _≡_ _≡_ f -inverseʳ⇒injective f = C.inverseʳ⇒injective _≡_ f refl sym trans - ------------------------------------------------------------------------- --- Inverseᵇ - -inverseᵇ⇒bijective : Inverseᵇ _≡_ _≡_ f f⁻¹ → Bijective _≡_ _≡_ f -inverseᵇ⇒bijective = C.inverseᵇ⇒bijective _≡_ refl sym trans - ------------------------------------------------------------------------- --- StrictlySurjective - -surjective⇒strictlySurjective : Surjective _≡_ _≡_ f → - StrictlySurjective _≡_ f -surjective⇒strictlySurjective = - C.surjective⇒strictlySurjective _≡_ refl +-- Properties that rely on congruence strictlySurjective⇒surjective : StrictlySurjective _≡_ f → Surjective _≡_ _≡_ f strictlySurjective⇒surjective = - C.strictlySurjective⇒surjective trans (cong _) + SetoidConsequences.strictlySurjective⇒surjective (cong _) ------------------------------------------------------------------------- --- StrictlyInverseˡ -inverseˡ⇒strictlyInverseˡ : Inverseˡ _≡_ _≡_ f f⁻¹ → - StrictlyInverseˡ _≡_ f f⁻¹ -inverseˡ⇒strictlyInverseˡ = - C.inverseˡ⇒strictlyInverseˡ _≡_ _≡_ refl - -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ʳ + SetoidConsequences.strictlyInverseˡ⇒inverseˡ (cong _) -inverseʳ⇒strictlyInverseʳ : Inverseʳ _≡_ _≡_ f f⁻¹ → - StrictlyInverseʳ _≡_ f f⁻¹ -inverseʳ⇒strictlyInverseʳ = C.inverseʳ⇒strictlyInverseʳ _≡_ _≡_ refl -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 = + SetoidConsequences.strictlyInverseʳ⇒inverseʳ (cong _) diff --git a/src/Function/Consequences/Setoid.agda b/src/Function/Consequences/Setoid.agda new file mode 100644 index 0000000000..229a565083 --- /dev/null +++ b/src/Function/Consequences/Setoid.agda @@ -0,0 +1,90 @@ +------------------------------------------------------------------------ +-- 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 + +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 + +open C public + using (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 (_⊔_) ------------------------------------------------------------------------ From f2747c47a2a92505ff9c0512aba3813be97c2efc Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Thu, 2 Nov 2023 12:12:31 +0900 Subject: [PATCH 2/6] Fix comment --- src/Data/Product/Function/Dependent/Setoid.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda index 1779a99915..22cb950626 100644 --- a/src/Data/Product/Function/Dependent/Setoid.agda +++ b/src/Data/Product/Function/Dependent/Setoid.agda @@ -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ʳ (I ×ₛ A) (J ×ₛ B) (Equivalence.from-cong equiv) strictlyInvʳ -- (Equivalence.from equiv) + invʳ = strictlyInverseʳ⇒inverseʳ (I ×ₛ A) (J ×ₛ B) (Equivalence.from-cong equiv) strictlyInvʳ ------------------------------------------------------------------------ From 48ff426dc6180044b93e439b674f72edae4026f3 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Thu, 2 Nov 2023 12:39:58 +0900 Subject: [PATCH 3/6] Fix re-export bug --- src/Function/Consequences/Propositional.agda | 61 +++++++++++--------- 1 file changed, 35 insertions(+), 26 deletions(-) diff --git a/src/Function/Consequences/Propositional.agda b/src/Function/Consequences/Propositional.agda index 1bdc31410e..302c0ca62c 100644 --- a/src/Function/Consequences/Propositional.agda +++ b/src/Function/Consequences/Propositional.agda @@ -7,47 +7,56 @@ {-# OPTIONS --cubical-compatible --safe #-} -module Function.Consequences.Propositional - {a b} {A : Set a} {B : Set b} where +module Function.Consequences.Propositional where open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong) open import Relation.Binary.PropositionalEquality.Properties using (setoid) open import Function.Definitions -import Function.Consequences.Setoid (setoid A) (setoid B) as SetoidConsequences +import Function.Consequences as Consequences +import Function.Consequences.Setoid as SetoidConsequences + +------------------------------------------------------------------------ +-- Re-export basic properties + +open Consequences public + using (contraInjective) -private - variable - f : A → B - f⁻¹ : B → A - ------------------------------------------------------------------------ -- Re-export setoid properties -open SetoidConsequences public - hiding - ( strictlySurjective⇒surjective - ; strictlyInverseˡ⇒inverseˡ - ; strictlyInverseʳ⇒inverseʳ - ) +module _ {a b} {A : Set a} {B : Set b} where + + open module App = SetoidConsequences (setoid A) (setoid B) public + hiding + ( strictlySurjective⇒surjective + ; strictlyInverseˡ⇒inverseˡ + ; strictlyInverseʳ⇒inverseʳ + ; contraInjective + ) ------------------------------------------------------------------------ -- Properties that rely on congruence -strictlySurjective⇒surjective : StrictlySurjective _≡_ f → - Surjective _≡_ _≡_ f -strictlySurjective⇒surjective = - SetoidConsequences.strictlySurjective⇒surjective (cong _) + private + variable + f : A → B + f⁻¹ : B → A + + strictlySurjective⇒surjective : StrictlySurjective _≡_ f → + Surjective _≡_ _≡_ f + strictlySurjective⇒surjective = + App.strictlySurjective⇒surjective (cong _) -strictlyInverseˡ⇒inverseˡ : ∀ f → StrictlyInverseˡ _≡_ f f⁻¹ → - Inverseˡ _≡_ _≡_ f f⁻¹ -strictlyInverseˡ⇒inverseˡ f = - SetoidConsequences.strictlyInverseˡ⇒inverseˡ (cong _) + strictlyInverseˡ⇒inverseˡ : ∀ f → StrictlyInverseˡ _≡_ f f⁻¹ → + Inverseˡ _≡_ _≡_ f f⁻¹ + strictlyInverseˡ⇒inverseˡ f = + App.strictlyInverseˡ⇒inverseˡ (cong _) -strictlyInverseʳ⇒inverseʳ : ∀ f → StrictlyInverseʳ _≡_ f f⁻¹ → - Inverseʳ _≡_ _≡_ f f⁻¹ -strictlyInverseʳ⇒inverseʳ f = - SetoidConsequences.strictlyInverseʳ⇒inverseʳ (cong _) + strictlyInverseʳ⇒inverseʳ : ∀ f → StrictlyInverseʳ _≡_ f f⁻¹ → + Inverseʳ _≡_ _≡_ f f⁻¹ + strictlyInverseʳ⇒inverseʳ f = + App.strictlyInverseʳ⇒inverseʳ (cong _) From 48129688c7c9f4a7f27265d8d3f2b188b2ee5ce5 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Thu, 2 Nov 2023 16:22:36 +0900 Subject: [PATCH 4/6] Finally fixed bug I hope --- CHANGELOG.md | 1 + src/Data/Fin/Properties.agda | 2 +- src/Function/Consequences.agda | 4 +- src/Function/Consequences/Propositional.agda | 69 +++++++++----------- src/Function/Consequences/Setoid.agda | 7 +- 5 files changed, 41 insertions(+), 42 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b7d88b83d0..7cda9fde57 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2013,6 +2013,7 @@ New modules ``` Function.Consequences Function.Consequences.Setoid + Function.Consequences.Propositional Function.Properties.Bijection Function.Properties.RightInverse Function.Properties.Surjection diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index cdcbeb4e85..ae616a7632 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -1010,7 +1010,7 @@ injective⇒≤ {zero} {_} {f} _ = z≤n injective⇒≤ {suc _} {zero} {f} _ = contradiction (f zero) ¬Fin0 injective⇒≤ {suc _} {suc _} {f} inj = s≤s (injective⇒≤ (λ eq → suc-injective (inj (punchOut-injective - (contraInjective inj 0≢1+n) + (contraInjective inj 0≢1+n) --(contraInjective inj 0≢1+n) (contraInjective inj 0≢1+n) eq)))) <⇒notInjective : ∀ {f : Fin m → Fin n} → n ℕ.< m → ¬ (Injective _≡_ _≡_ f) 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 302c0ca62c..ba583ccdeb 100644 --- a/src/Function/Consequences/Propositional.agda +++ b/src/Function/Consequences/Propositional.agda @@ -7,56 +7,51 @@ {-# 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.Core using (_≡_; _≢_; cong) open import Relation.Binary.PropositionalEquality.Properties using (setoid) open import Function.Definitions +open import Relation.Nullary.Negation.Core using (contraposition) -import Function.Consequences as Consequences -import Function.Consequences.Setoid as SetoidConsequences +import Function.Consequences.Setoid (setoid A) (setoid B) + as Setoid ------------------------------------------------------------------------ -- Re-export basic properties -open Consequences public - using (contraInjective) - ------------------------------------------------------------------------ -- Re-export setoid properties -module _ {a b} {A : Set a} {B : Set b} where - - open module App = SetoidConsequences (setoid A) (setoid B) public - hiding - ( strictlySurjective⇒surjective - ; strictlyInverseˡ⇒inverseˡ - ; strictlyInverseʳ⇒inverseʳ - ; contraInjective - ) +open Setoid public + hiding + ( strictlySurjective⇒surjective + ; strictlyInverseˡ⇒inverseˡ + ; strictlyInverseʳ⇒inverseʳ + ) ------------------------------------------------------------------------ -- Properties that rely on congruence - private - variable - f : A → B - f⁻¹ : B → A - - strictlySurjective⇒surjective : StrictlySurjective _≡_ f → - Surjective _≡_ _≡_ f - strictlySurjective⇒surjective = - App.strictlySurjective⇒surjective (cong _) - - - strictlyInverseˡ⇒inverseˡ : ∀ f → StrictlyInverseˡ _≡_ f f⁻¹ → - Inverseˡ _≡_ _≡_ f f⁻¹ - strictlyInverseˡ⇒inverseˡ f = - App.strictlyInverseˡ⇒inverseˡ (cong _) - - - strictlyInverseʳ⇒inverseʳ : ∀ f → StrictlyInverseʳ _≡_ f f⁻¹ → - Inverseʳ _≡_ _≡_ f f⁻¹ - strictlyInverseʳ⇒inverseʳ f = - App.strictlyInverseʳ⇒inverseʳ (cong _) +private + variable + f : A → B + f⁻¹ : B → A + +strictlySurjective⇒surjective : StrictlySurjective _≡_ f → + Surjective _≡_ _≡_ f +strictlySurjective⇒surjective = + Setoid.strictlySurjective⇒surjective (cong _) + +strictlyInverseˡ⇒inverseˡ : ∀ f → StrictlyInverseˡ _≡_ f f⁻¹ → + Inverseˡ _≡_ _≡_ f f⁻¹ +strictlyInverseˡ⇒inverseˡ f = + Setoid.strictlyInverseˡ⇒inverseˡ (cong _) + +strictlyInverseʳ⇒inverseʳ : ∀ f → StrictlyInverseʳ _≡_ f f⁻¹ → + Inverseʳ _≡_ _≡_ f f⁻¹ +strictlyInverseʳ⇒inverseʳ f = + Setoid.strictlyInverseʳ⇒inverseʳ (cong _) diff --git a/src/Function/Consequences/Setoid.agda b/src/Function/Consequences/Setoid.agda index 229a565083..6c47d73dfd 100644 --- a/src/Function/Consequences/Setoid.agda +++ b/src/Function/Consequences/Setoid.agda @@ -16,6 +16,7 @@ module Function.Consequences.Setoid where open import Function.Definitions +open import Relation.Nullary.Negation.Core import Function.Consequences as C @@ -30,8 +31,10 @@ private ------------------------------------------------------------------------ -- Injective -open C public - using (contraInjective) +-- For some reason, exporting this doesn't +contraInjective : Injective ≈₁ ≈₂ f → + ∀ {x y} → ¬ (≈₁ x y) → ¬ (≈₂ (f x) (f y)) +contraInjective = C.contraInjective ≈₂ ------------------------------------------------------------------------ -- Inverseˡ From 465c52f27a9295187497089f0720e9a97913b4f2 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Thu, 2 Nov 2023 16:24:12 +0900 Subject: [PATCH 5/6] Removed rogue comment --- src/Data/Fin/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index ae616a7632..cdcbeb4e85 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -1010,7 +1010,7 @@ injective⇒≤ {zero} {_} {f} _ = z≤n injective⇒≤ {suc _} {zero} {f} _ = contradiction (f zero) ¬Fin0 injective⇒≤ {suc _} {suc _} {f} inj = s≤s (injective⇒≤ (λ eq → suc-injective (inj (punchOut-injective - (contraInjective inj 0≢1+n) --(contraInjective inj 0≢1+n) + (contraInjective inj 0≢1+n) (contraInjective inj 0≢1+n) eq)))) <⇒notInjective : ∀ {f : Fin m → Fin n} → n ℕ.< m → ¬ (Injective _≡_ _≡_ f) From 01dedd83f7b8c871e8dc55ff70c1eb289de78f8f Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Thu, 2 Nov 2023 16:25:41 +0900 Subject: [PATCH 6/6] More tidying up --- src/Function/Consequences/Propositional.agda | 6 +----- src/Function/Consequences/Setoid.agda | 1 - 2 files changed, 1 insertion(+), 6 deletions(-) diff --git a/src/Function/Consequences/Propositional.agda b/src/Function/Consequences/Propositional.agda index ba583ccdeb..a2558a9c48 100644 --- a/src/Function/Consequences/Propositional.agda +++ b/src/Function/Consequences/Propositional.agda @@ -17,11 +17,7 @@ open import Relation.Binary.PropositionalEquality.Properties open import Function.Definitions open import Relation.Nullary.Negation.Core using (contraposition) -import Function.Consequences.Setoid (setoid A) (setoid B) - as Setoid - ------------------------------------------------------------------------- --- Re-export basic properties +import Function.Consequences.Setoid (setoid A) (setoid B) as Setoid ------------------------------------------------------------------------ -- Re-export setoid properties diff --git a/src/Function/Consequences/Setoid.agda b/src/Function/Consequences/Setoid.agda index 6c47d73dfd..d2c3b948d9 100644 --- a/src/Function/Consequences/Setoid.agda +++ b/src/Function/Consequences/Setoid.agda @@ -31,7 +31,6 @@ private ------------------------------------------------------------------------ -- Injective --- For some reason, exporting this doesn't contraInjective : Injective ≈₁ ≈₂ f → ∀ {x y} → ¬ (≈₁ x y) → ¬ (≈₂ (f x) (f y)) contraInjective = C.contraInjective ≈₂