# Split surjective maps

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Elif Uskuplu.

Created on 2022-01-26.

module foundation.split-surjective-maps where
Imports
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.injective-maps
open import foundation-core.retractions
open import foundation-core.sections
open import foundation-core.type-theoretic-principle-of-choice

## Idea

A map f : A → B is split surjective if we can construct for every b : B an element in the fiber of b, meaning an element a : A equipped with an identification f a ＝ b.

## Warning

Note that split-surjectiveness is the Curry-Howard interpretation of surjectiveness. However, this is not a property, and the split surjective maps don't fit in a factorization system along with the injective maps.

## Definition

### Split surjective maps

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

is-split-surjective : (A  B)  UU (l1  l2)
is-split-surjective f = (b : B)  fiber f b

split-surjection : UU (l1  l2)
split-surjection = Σ (A  B) is-split-surjective

map-split-surjection : split-surjection  (A  B)
map-split-surjection = pr1

is-split-surjective-split-surjection :
(f : split-surjection)  is-split-surjective (map-split-surjection f)
is-split-surjective-split-surjection = pr2

## Properties

### Split surjections are equivalent to maps equipped with a section

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B)
where

section-is-split-surjective : is-split-surjective f  section f
pr1 (section-is-split-surjective s) = pr1  s
pr2 (section-is-split-surjective s) = pr2  s

is-split-surjective-section : section f  is-split-surjective f
pr1 (is-split-surjective-section s b) = pr1 s b
pr2 (is-split-surjective-section s b) = pr2 s b

equiv-section-is-split-surjective : is-split-surjective f  section f
equiv-section-is-split-surjective = distributive-Π-Σ

equiv-is-split-surjective-section : section f  is-split-surjective f
equiv-is-split-surjective-section = inv-distributive-Π-Σ

### A map is an equivalence if and only if it is injective and split surjective

module _
{l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X  Y)
where

retraction-is-split-surjective-is-injective :
is-injective f  is-split-surjective f  retraction f
pr1 (retraction-is-split-surjective-is-injective l s) = pr1  s
pr2 (retraction-is-split-surjective-is-injective l s) = l  (pr2  (s  f))

is-equiv-is-split-surjective-is-injective :
is-injective f  is-split-surjective f  is-equiv f
pr1 (is-equiv-is-split-surjective-is-injective l s) =
section-is-split-surjective f s
pr2 (is-equiv-is-split-surjective-is-injective l s) =
retraction-is-split-surjective-is-injective l s

is-split-surjective-is-equiv : is-equiv f  is-split-surjective f
is-split-surjective-is-equiv = is-split-surjective-section f  pr1

is-split-surjective-is-injective-is-equiv :
is-equiv f  is-injective f × is-split-surjective f
pr1 (is-split-surjective-is-injective-is-equiv is-equiv-f) =
is-injective-is-equiv is-equiv-f
pr2 (is-split-surjective-is-injective-is-equiv is-equiv-f) =
is-split-surjective-is-equiv is-equiv-f