Connect LeftInverse with (Split)Surjection (agda#2054)

Author: laMudri

CHANGELOG.md

@@ -3238,6 +3238,13 @@ Additions to existing modules
   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 application operator synonym to `Function.Bundles`:
   ```agda
@@ -3260,6 +3267,12 @@ Additions to existing modules
   _!|>_  : (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`:
   ```

src/Function/Bundles.agda

@@ -218,14 +218,28 @@ 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
       { to-cong   = to-cong
       ; from-cong = from-cong
       }
 
+    isSplitSurjection : IsSplitSurjection to
+    isSplitSurjection = record
+      { from = from
+      ; isLeftInverse = isLeftInverse
+      }
+
+    surjection : Surjection From To
+    surjection = record
+      { to = to
+      ; cong = to-cong
+      ; surjective = λ y → from y , inverseˡ
+      }
+
+
 
   record RightInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field
@@ -346,6 +360,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

src/Function/Structures.agda

@@ -107,6 +107,12 @@ 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ˡ
+    }
+
 
 record IsRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
   field
@@ -168,3 +174,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