From 5e8aa87f551e89e9f9377365f44e4c56e373593e Mon Sep 17 00:00:00 2001 From: James Wood Date: Sun, 13 Aug 2023 12:02:42 +0100 Subject: [PATCH 1/3] connect LeftInverse with (Split)Surjection --- CHANGELOG.md | 15 ++++++++++++- src/Function/Bundles.agda | 42 +++++++++++++++++++++++++++++++++++- src/Function/Structures.agda | 16 ++++++++++++++ 3 files changed, 71 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5394b704d0..07f494d564 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2658,7 +2658,7 @@ Other minor changes ∀ {m n} → _Respectsʳ_ (_<_ {m} {n}) _≋_ <-wellFounded : Symmetric _≈_ → Transitive _≈_ → _≺_ Respectsʳ _≈_ → WellFounded _≺_ → ∀ {n} → WellFounded (_<_ {n}) -``` + ``` * Added new functions in `Data.Vec.Relation.Unary.Any`: ``` @@ -2681,6 +2681,13 @@ Other minor changes evalState : State s a → s → a execState : State s a → s → s ``` + +* Added new proofs and definitions in `Function.Bundles`: + ```agda + LeftInverse.isSplitSurjection : LeftInverse → IsSplitSurjection to + LeftInverse.surjection : LeftInverse → Surjection + SplitSurjection = LeftInverse + ``` * Added new proofs in `Function.Construct.Symmetry`: ``` @@ -2697,6 +2704,12 @@ Other minor changes _!|>_ : (a : A) → (∀ a → B a) → B a _!|>′_ : A → (A → B) → B ``` + +* Added new proof and record in `Function.Structures`: + ```agda + IsLeftInverse.isSurjection : IsLeftInverse to from → IsSurjection to + record IsSplitSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) + ``` * Added new definition to the `Surjection` module in `Function.Related.Surjection`: ``` diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index 1b92bee909..26b2324cfc 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -188,7 +188,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where } open IsLeftInverse isLeftInverse public - using (module Eq₁; module Eq₂; strictlyInverseˡ) + using (module Eq₁; module Eq₂; strictlyInverseˡ; isSurjection) equivalence : Equivalence equivalence = record @@ -196,6 +196,46 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where ; from-cong = from-cong } + isSplitSurjection : IsSplitSurjection to + isSplitSurjection = record { from = from ; isLeftInverse = isLeftInverse } + + surjection : Surjection + surjection = record + { to = to + ; cong = to-cong + ; surjective = λ y → from y , inverseˡ + } + + -- A left inverse is also known as a “split surjection”. + -- As the name implies, a split surjection is a special kind of surjection, as + -- shown by the definition `LeftInverse.surjection` above. + -- The difference is the `from-cong` law --- generally, the section (called + -- `Surjection.to⁻` 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 + -- propositional equality (because all functions respect propositional + -- equality). + -- + -- For further background on (split) surjections, one may consult any general + -- mathematical references which work without the principle of choice. + -- For example, https://ncatlab.org/nlab/show/split+epimorphism. + -- The connection to set-theoretic notions with the same names is justified by + -- the setoid type theory/homotopy type theory observation/definition that + -- (∃x : A. P) = ∥ Σx : A. P ∥ --- i.e., that we can read set-theoretic ∃ as + -- squashed/propositionally truncated Σ. + -- We see working with setoids as working in the MLTT model of a setoid type + -- theory, in which ∥ X ∥ is interpreted as the setoid with carrier set X and + -- the equivalence relation that relates all elements. + -- All maps into ∥ X ∥ respect equality, so in the idiomatic definitions here, + -- we drop the corresponding trivial `cong` field completely. + + SplitSurjection : Set _ + SplitSurjection = LeftInverse + + module SplitSurjection (splitSurjection : SplitSurjection) = + LeftInverse splitSurjection + record RightInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index 5566e92c8b..c5042d3b6f 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -105,6 +105,22 @@ record IsLeftInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from strictlyInverseˡ x = inverseˡ Eq₁.refl + isSurjection : IsSurjection to + isSurjection = record + { isCongruent = isCongruent + ; surjective = λ y → from y , inverseˡ + } + +-- See the comment on `SplitSurjection` in `Function.Bundles` for an explanation +-- of (split) surjections. + +record IsSplitSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where + field + from : B → A + isLeftInverse : IsLeftInverse f from + + open IsLeftInverse isLeftInverse public + record IsRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field From 5e8c0a2813fc6ebf87a387792de2128533e2cdbe Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Thu, 19 Oct 2023 10:54:08 +0900 Subject: [PATCH 2/3] Touch up docs --- src/Function/Bundles.agda | 73 +++++++++++++++++++++--------------- src/Function/Structures.agda | 24 +++++++----- 2 files changed, 57 insertions(+), 40 deletions(-) diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index 26b2324cfc..e190559423 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -197,7 +197,10 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where } isSplitSurjection : IsSplitSurjection to - isSplitSurjection = record { from = from ; isLeftInverse = isLeftInverse } + isSplitSurjection = record + { from = from + ; isLeftInverse = isLeftInverse + } surjection : Surjection surjection = record @@ -206,35 +209,6 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where ; surjective = λ y → from y , inverseˡ } - -- A left inverse is also known as a “split surjection”. - -- As the name implies, a split surjection is a special kind of surjection, as - -- shown by the definition `LeftInverse.surjection` above. - -- The difference is the `from-cong` law --- generally, the section (called - -- `Surjection.to⁻` 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 - -- propositional equality (because all functions respect propositional - -- equality). - -- - -- For further background on (split) surjections, one may consult any general - -- mathematical references which work without the principle of choice. - -- For example, https://ncatlab.org/nlab/show/split+epimorphism. - -- The connection to set-theoretic notions with the same names is justified by - -- the setoid type theory/homotopy type theory observation/definition that - -- (∃x : A. P) = ∥ Σx : A. P ∥ --- i.e., that we can read set-theoretic ∃ as - -- squashed/propositionally truncated Σ. - -- We see working with setoids as working in the MLTT model of a setoid type - -- theory, in which ∥ X ∥ is interpreted as the setoid with carrier set X and - -- the equivalence relation that relates all elements. - -- All maps into ∥ X ∥ respect equality, so in the idiomatic definitions here, - -- we drop the corresponding trivial `cong` field completely. - - SplitSurjection : Set _ - SplitSurjection = LeftInverse - - module SplitSurjection (splitSurjection : SplitSurjection) = - LeftInverse splitSurjection record RightInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where @@ -356,6 +330,45 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where ; from₂-cong = from₂-cong } +------------------------------------------------------------------------ +-- Other + + -- A left inverse is also known as a “split surjection”. + -- + -- As the name implies, a split surjection is a special kind of + -- surjection where the witness generated in the domain in the + -- 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 + -- need not respect equality, whereas it must in a split surjection. + -- + -- The two notions coincide when the equivalence relation on `B` is + -- propositional equality (because all functions respect propositional + -- equality). + -- + -- For further background on (split) surjections, one may consult any + -- general mathematical references which work without the principle + -- of choice. For example: + -- + -- https://ncatlab.org/nlab/show/split+epimorphism. + -- + -- The connection to set-theoretic notions with the same names is + -- justified by the setoid type theory/homotopy type theory + -- observation/definition that (∃x : A. P) = ∥ Σx : A. P ∥ --- i.e., + -- we can read set-theoretic ∃ as squashed/propositionally truncated Σ. + -- + -- We see working with setoids as working in the MLTT model of a setoid + -- type theory, in which ∥ X ∥ is interpreted as the setoid with carrier + -- set X and the equivalence relation that relates all elements. + -- All maps into ∥ X ∥ respect equality, so in the idiomatic definitions + -- here, we drop the corresponding trivial `cong` field completely. + + SplitSurjection : Set _ + SplitSurjection = LeftInverse + + module SplitSurjection (splitSurjection : SplitSurjection) = + LeftInverse splitSurjection ------------------------------------------------------------------------ -- Bundles specialised for propositional equality diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index c5042d3b6f..a859227868 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -111,16 +111,6 @@ record IsLeftInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ; surjective = λ y → from y , inverseˡ } --- See the comment on `SplitSurjection` in `Function.Bundles` for an explanation --- of (split) surjections. - -record IsSplitSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where - field - from : B → A - isLeftInverse : IsLeftInverse f from - - open IsLeftInverse isLeftInverse public - record IsRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field @@ -182,3 +172,17 @@ record IsBiInverse open IsCongruent to-isCongruent public renaming (cong to to-cong) + + +------------------------------------------------------------------------ +-- Other +------------------------------------------------------------------------ + +-- See the comment on `SplitSurjection` in `Function.Bundles` for an +-- explanation of (split) surjections. +record IsSplitSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where + field + from : B → A + isLeftInverse : IsLeftInverse f from + + open IsLeftInverse isLeftInverse public From 26abba3638d3d8df21e80833194c8187d7516d85 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Thu, 19 Oct 2023 11:01:51 +0900 Subject: [PATCH 3/3] Fix merge conflict --- src/Function/Bundles.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index bf885a28e0..9e18c30fe5 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -232,7 +232,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where ; isLeftInverse = isLeftInverse } - surjection : Surjection + surjection : Surjection From To surjection = record { to = to ; cong = to-cong