Connect LeftInverse with (Split)Surjection

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`:
   ```

src/Function/Bundles.agda

@@ -188,14 +188,54 @@ 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
+    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

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