# Surjective maps

```agda
module foundation.surjective-maps where
```

<details><summary>Imports</summary>

```agda
open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.connected-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.dependent-universal-property-equivalences
open import foundation.embeddings
open import foundation.equality-cartesian-product-types
open import foundation.function-extensionality
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.monomorphisms
open import foundation.propositional-truncations
open import foundation.split-surjective-maps
open import foundation.structure-identity-principle
open import foundation.subtype-identity-principle
open import foundation.subtypes
open import foundation.truncated-types
open import foundation.type-theoretic-principle-of-choice
open import foundation.univalence
open import foundation.universal-property-dependent-pair-types
open import foundation.universal-property-propositional-truncation
open import foundation.universe-levels

open import foundation-core.constant-maps
open import foundation-core.contractible-maps
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-function-types
open import foundation-core.precomposition-dependent-functions
open import foundation-core.propositional-maps
open import foundation-core.propositions
open import foundation-core.sections
open import foundation-core.sets
open import foundation-core.torsorial-type-families
open import foundation-core.truncated-maps
open import foundation-core.truncation-levels

open import orthogonal-factorization-systems.extensions-of-maps
```

</details>

## Idea

A map `f : A → B` is **surjective** if all of its
[fibers](foundation-core.fibers-of-maps.md) are
[inhabited](foundation.inhabited-types.md).

## Definition

### Surjective maps

```agda
is-surjective-Prop :
  {l1 l2 : Level} {A : UU l1} {B : UU l2}  (A  B)  Prop (l1  l2)
is-surjective-Prop {B = B} f = Π-Prop B (trunc-Prop  fiber f)

is-surjective :
  {l1 l2 : Level} {A : UU l1} {B : UU l2}  (A  B)  UU (l1  l2)
is-surjective f = type-Prop (is-surjective-Prop f)

is-prop-is-surjective :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
  is-prop (is-surjective f)
is-prop-is-surjective f = is-prop-type-Prop (is-surjective-Prop f)

infix 5 _↠_
_↠_ : {l1 l2 : Level}  UU l1  UU l2  UU (l1  l2)
A  B = Σ (A  B) is-surjective

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

  map-surjection : A  B
  map-surjection = pr1 f

  is-surjective-map-surjection : is-surjective map-surjection
  is-surjective-map-surjection = pr2 f
```

### The type of all surjective maps out of a type

```agda
Surjection : {l1 : Level} (l2 : Level)  UU l1  UU (l1  lsuc l2)
Surjection l2 A = Σ (UU l2) (A ↠_)

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

  type-Surjection : UU l2
  type-Surjection = pr1 f

  surjection-Surjection : A  type-Surjection
  surjection-Surjection = pr2 f

  map-Surjection : A  type-Surjection
  map-Surjection = map-surjection surjection-Surjection

  is-surjective-map-Surjection : is-surjective map-Surjection
  is-surjective-map-Surjection =
    is-surjective-map-surjection surjection-Surjection
```

### The type of all surjective maps into `k`-truncated types

```agda
Surjection-Into-Truncated-Type :
  {l1 : Level} (l2 : Level) (k : 𝕋)  UU l1  UU (l1  lsuc l2)
Surjection-Into-Truncated-Type l2 k A =
  Σ (Truncated-Type l2 k)  X  A  type-Truncated-Type X)

emb-inclusion-Surjection-Into-Truncated-Type :
  {l1 : Level} (l2 : Level) (k : 𝕋) (A : UU l1) 
  Surjection-Into-Truncated-Type l2 k A  Surjection l2 A
emb-inclusion-Surjection-Into-Truncated-Type l2 k A =
  emb-Σ  X  A  X) (emb-type-Truncated-Type l2 k)  X  id-emb)

inclusion-Surjection-Into-Truncated-Type :
  {l1 l2 : Level} {k : 𝕋} {A : UU l1} 
  Surjection-Into-Truncated-Type l2 k A  Surjection l2 A
inclusion-Surjection-Into-Truncated-Type {l1} {l2} {k} {A} =
  map-emb (emb-inclusion-Surjection-Into-Truncated-Type l2 k A)

module _
  {l1 l2 : Level} {k : 𝕋} {A : UU l1}
  (f : Surjection-Into-Truncated-Type l2 k A)
  where

  truncated-type-Surjection-Into-Truncated-Type : Truncated-Type l2 k
  truncated-type-Surjection-Into-Truncated-Type = pr1 f

  type-Surjection-Into-Truncated-Type : UU l2
  type-Surjection-Into-Truncated-Type =
    type-Truncated-Type truncated-type-Surjection-Into-Truncated-Type

  is-trunc-type-Surjection-Into-Truncated-Type :
    is-trunc k type-Surjection-Into-Truncated-Type
  is-trunc-type-Surjection-Into-Truncated-Type =
    is-trunc-type-Truncated-Type
      truncated-type-Surjection-Into-Truncated-Type

  surjection-Surjection-Into-Truncated-Type :
    A  type-Surjection-Into-Truncated-Type
  surjection-Surjection-Into-Truncated-Type = pr2 f

  map-Surjection-Into-Truncated-Type :
    A  type-Surjection-Into-Truncated-Type
  map-Surjection-Into-Truncated-Type =
    map-surjection surjection-Surjection-Into-Truncated-Type

  is-surjective-Surjection-Into-Truncated-Type :
    is-surjective map-Surjection-Into-Truncated-Type
  is-surjective-Surjection-Into-Truncated-Type =
    is-surjective-map-surjection surjection-Surjection-Into-Truncated-Type
```

### The type of all surjective maps into sets

```agda
Surjection-Into-Set :
  {l1 : Level} (l2 : Level)  UU l1  UU (l1  lsuc l2)
Surjection-Into-Set l2 A = Surjection-Into-Truncated-Type l2 zero-𝕋 A

emb-inclusion-Surjection-Into-Set :
  {l1 : Level} (l2 : Level) (A : UU l1) 
  Surjection-Into-Set l2 A  Surjection l2 A
emb-inclusion-Surjection-Into-Set l2 A =
  emb-inclusion-Surjection-Into-Truncated-Type l2 zero-𝕋 A

inclusion-Surjection-Into-Set :
  {l1 l2 : Level} {A : UU l1} 
  Surjection-Into-Set l2 A  Surjection l2 A
inclusion-Surjection-Into-Set {l1} {l2} {A} =
  inclusion-Surjection-Into-Truncated-Type

module _
  {l1 l2 : Level} {A : UU l1} (f : Surjection-Into-Set l2 A)
  where

  set-Surjection-Into-Set : Set l2
  set-Surjection-Into-Set = truncated-type-Surjection-Into-Truncated-Type f

  type-Surjection-Into-Set : UU l2
  type-Surjection-Into-Set = type-Surjection-Into-Truncated-Type f

  is-set-type-Surjection-Into-Set : is-set type-Surjection-Into-Set
  is-set-type-Surjection-Into-Set =
    is-trunc-type-Surjection-Into-Truncated-Type f

  surjection-Surjection-Into-Set : A  type-Surjection-Into-Set
  surjection-Surjection-Into-Set = surjection-Surjection-Into-Truncated-Type f

  map-Surjection-Into-Set : A  type-Surjection-Into-Set
  map-Surjection-Into-Set = map-Surjection-Into-Truncated-Type f

  is-surjective-Surjection-Into-Set : is-surjective map-Surjection-Into-Set
  is-surjective-Surjection-Into-Set =
    is-surjective-Surjection-Into-Truncated-Type f
```

## Properties

### Any map that has a section is surjective

```agda
abstract
  is-surjective-has-section :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B} 
    section f  is-surjective f
  is-surjective-has-section (g , G) b = unit-trunc-Prop (g b , G b)
```

### Any split surjective map is surjective

```agda
abstract
  is-surjective-is-split-surjective :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B} 
    is-split-surjective f  is-surjective f
  is-surjective-is-split-surjective H x =
    unit-trunc-Prop (H x)
```

### Any equivalence is surjective

```agda
is-surjective-is-equiv :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B} 
  is-equiv f  is-surjective f
is-surjective-is-equiv H = is-surjective-has-section (pr1 H)

is-surjective-map-equiv :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A  B) 
  is-surjective (map-equiv e)
is-surjective-map-equiv e = is-surjective-is-equiv (is-equiv-map-equiv e)
```

### The identity function is surjective

```agda
module _
  {l : Level} {A : UU l}
  where

  is-surjective-id : is-surjective (id {A = A})
  is-surjective-id a = unit-trunc-Prop (a , refl)
```

### Maps which are homotopic to surjective maps are surjective

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

  abstract
    is-surjective-htpy :
      {f g : A  B}  f ~ g  is-surjective g  is-surjective f
    is-surjective-htpy {f} {g} H K b =
      apply-universal-property-trunc-Prop
        ( K b)
        ( trunc-Prop (fiber f b))
        ( λ where (a , refl)  unit-trunc-Prop (a , H a))

  abstract
    is-surjective-htpy' :
      {f g : A  B}  f ~ g  is-surjective f  is-surjective g
    is-surjective-htpy' H = is-surjective-htpy (inv-htpy H)
```

### The dependent universal property of surjective maps

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

  dependent-universal-property-surj : UUω
  dependent-universal-property-surj =
    {l : Level} (P : B  Prop l) 
    is-equiv  (h : (b : B)  type-Prop (P b)) x  h (f x))

  abstract
    is-surjective-dependent-universal-property-surj :
      dependent-universal-property-surj  is-surjective f
    is-surjective-dependent-universal-property-surj dup-surj-f =
      map-inv-is-equiv
        ( dup-surj-f  b  trunc-Prop (fiber f b)))
        ( λ x  unit-trunc-Prop (x , refl))

  abstract
    square-dependent-universal-property-surj :
      {l3 : Level} (P : B  Prop l3) 
      ( λ (h : (y : B)  type-Prop (P y)) x  h (f x)) ~
      ( ( λ h x  h (f x) (x , refl)) 
        ( λ h y  (h y)  unit-trunc-Prop) 
        ( λ h y  const (type-trunc-Prop (fiber f y)) (type-Prop (P y)) (h y)))
    square-dependent-universal-property-surj P = refl-htpy

  abstract
    dependent-universal-property-surj-is-surjective :
      is-surjective f  dependent-universal-property-surj
    dependent-universal-property-surj-is-surjective is-surj-f P =
      is-equiv-comp
        ( λ h x  h (f x) (x , refl))
        ( ( λ h y  (h y)  unit-trunc-Prop) 
          ( λ h y 
            const (type-trunc-Prop (fiber f y)) (type-Prop (P y)) (h y)))
        ( is-equiv-comp
          ( λ h y  (h y)  unit-trunc-Prop)
          ( λ h y  const (type-trunc-Prop (fiber f y)) (type-Prop (P y)) (h y))
          ( is-equiv-map-Π-is-fiberwise-equiv
            ( λ y 
              is-equiv-diagonal-is-contr
                ( is-proof-irrelevant-is-prop
                  ( is-prop-type-trunc-Prop)
                  ( is-surj-f y))
                ( type-Prop (P y))))
          ( is-equiv-map-Π-is-fiberwise-equiv
            ( λ b  is-propositional-truncation-trunc-Prop (fiber f b) (P b))))
        ( is-equiv-map-reduce-Π-fiber f ( λ y z  type-Prop (P y)))

  equiv-dependent-universal-property-surj-is-surjective :
    is-surjective f 
    {l : Level} (C : B  Prop l) 
    ((b : B)  type-Prop (C b))  ((a : A)  type-Prop (C (f a)))
  pr1 (equiv-dependent-universal-property-surj-is-surjective H C) h x =
    h (f x)
  pr2 (equiv-dependent-universal-property-surj-is-surjective H C) =
    dependent-universal-property-surj-is-surjective H C

  apply-dependent-universal-property-surj-is-surjective :
    is-surjective f 
    {l : Level} (C : B  Prop l) 
    ((a : A)  type-Prop (C (f a)))  ((y : B)  type-Prop (C y))
  apply-dependent-universal-property-surj-is-surjective H C =
    map-inv-equiv (equiv-dependent-universal-property-surj-is-surjective H C)

  apply-twice-dependent-universal-property-surj-is-surjective :
    is-surjective f 
    {l : Level} (C : B  B  Prop l) 
    ((x y : A)  type-Prop (C (f x) (f y)))  ((s t : B)  type-Prop (C s t))
  apply-twice-dependent-universal-property-surj-is-surjective H C G s =
    apply-dependent-universal-property-surj-is-surjective
      ( H)
      ( λ b  C s b)
      ( λ y 
        apply-dependent-universal-property-surj-is-surjective
          ( H)
          ( λ b  C b (f y))
          ( λ x  G x y)
          ( s))

equiv-dependent-universal-property-surjection :
  {l l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
  (C : B  Prop l) 
  ((b : B)  type-Prop (C b))  ((a : A)  type-Prop (C (map-surjection f a)))
equiv-dependent-universal-property-surjection f =
  equiv-dependent-universal-property-surj-is-surjective
    ( map-surjection f)
    ( is-surjective-map-surjection f)

apply-dependent-universal-property-surjection :
  {l l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
  (C : B  Prop l) 
  ((a : A)  type-Prop (C (map-surjection f a)))  ((y : B)  type-Prop (C y))
apply-dependent-universal-property-surjection f =
  apply-dependent-universal-property-surj-is-surjective
    ( map-surjection f)
    ( is-surjective-map-surjection f)
```

### A map into a proposition is a propositional truncation if and only if it is surjective

```agda
abstract
  is-surjective-is-propositional-truncation :
    {l1 l2 : Level} {A : UU l1} {P : Prop l2} (f : A  type-Prop P) 
    ( {l : Level} 
      dependent-universal-property-propositional-truncation l P f) 
    is-surjective f
  is-surjective-is-propositional-truncation f duppt-f =
    is-surjective-dependent-universal-property-surj f duppt-f

abstract
  is-propsitional-truncation-is-surjective :
    {l1 l2 : Level} {A : UU l1} {P : Prop l2} (f : A  type-Prop P) 
    is-surjective f 
    {l : Level}  dependent-universal-property-propositional-truncation l P f
  is-propsitional-truncation-is-surjective f is-surj-f =
    dependent-universal-property-surj-is-surjective f is-surj-f
```

### A map that is both surjective and an embedding is an equivalence

```agda
abstract
  is-equiv-is-emb-is-surjective :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B} 
    is-surjective f  is-emb f  is-equiv f
  is-equiv-is-emb-is-surjective {f = f} H K =
    is-equiv-is-contr-map
      ( λ y 
        is-proof-irrelevant-is-prop
          ( is-prop-map-is-emb K y)
          ( apply-universal-property-trunc-Prop
            ( H y)
            ( fiber-emb-Prop (f , K) y)
            ( id)))
```

### The composite of surjective maps is surjective

```agda
module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  where

  abstract
    is-surjective-left-map-triangle :
      (f : A  X) (g : B  X) (h : A  B) (H : f ~ (g  h)) 
      is-surjective g  is-surjective h  is-surjective f
    is-surjective-left-map-triangle f g h H is-surj-g is-surj-h x =
      apply-universal-property-trunc-Prop
        ( is-surj-g x)
        ( trunc-Prop (fiber f x))
        ( λ where
          ( b , refl) 
            apply-universal-property-trunc-Prop
              ( is-surj-h b)
              ( trunc-Prop (fiber f (g b)))
              ( λ where (a , refl)  unit-trunc-Prop (a , H a)))

  is-surjective-comp :
    {g : B  X} {h : A  B} 
    is-surjective g  is-surjective h  is-surjective (g  h)
  is-surjective-comp {g} {h} =
    is-surjective-left-map-triangle (g  h) g h refl-htpy
```

### Functoriality of products preserves being surjective

```agda
module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  where

  is-surjective-map-prod :
    {f : A  C} {g : B  D} 
    is-surjective f  is-surjective g  is-surjective (map-prod f g)
  is-surjective-map-prod {f} {g} s s' (c , d) =
    apply-twice-universal-property-trunc-Prop
      ( s c)
      ( s' d)
      ( trunc-Prop (fiber (map-prod f g) (c , d)))
      ( λ x y 
        unit-trunc-Prop ((pr1 x , pr1 y) , eq-pair (pr2 x) (pr2 y)))

  surjection-prod :
    (A  C)  (B  D)  ((A × B)  (C × D))
  pr1 (surjection-prod f g) = map-prod (map-surjection f) (map-surjection g)
  pr2 (surjection-prod f g) =
    is-surjective-map-prod
      ( is-surjective-map-surjection f)
      ( is-surjective-map-surjection g)
```

### The composite of a surjective map with an equivalence is surjective

```agda
is-surjective-comp-equiv :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
  (e : B  C)  {f : A  B}  is-surjective f  is-surjective (map-equiv e  f)
is-surjective-comp-equiv e =
  is-surjective-comp (is-surjective-map-equiv e)
```

### The precomposite of a surjective map with an equivalence is surjective

```agda
is-surjective-precomp-equiv :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {f : B  C} 
  is-surjective f  (e : A  B)  is-surjective (f  map-equiv e)
is-surjective-precomp-equiv H e =
  is-surjective-comp H (is-surjective-map-equiv e)
```

### If a composite is surjective, then so is its left factor

```agda
module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  where

  abstract
    is-surjective-right-map-triangle :
      (f : A  X) (g : B  X) (h : A  B) (H : f ~ (g  h)) 
      is-surjective f  is-surjective g
    is-surjective-right-map-triangle f g h H is-surj-f x =
      apply-universal-property-trunc-Prop
        ( is-surj-f x)
        ( trunc-Prop (fiber g x))
        ( λ where (a , refl)  unit-trunc-Prop (h a , inv (H a)))

  is-surjective-left-factor :
    {g : B  X} (h : A  B)  is-surjective (g  h)  is-surjective g
  is-surjective-left-factor {g} h =
    is-surjective-right-map-triangle (g  h) g h refl-htpy
```

### Surjective maps are `-1`-connected

```agda
is-neg-one-connected-map-is-surjective :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B} 
  is-surjective f  is-connected-map neg-one-𝕋 f
is-neg-one-connected-map-is-surjective H b =
  is-proof-irrelevant-is-prop is-prop-type-trunc-Prop (H b)

is-surjective-is-neg-one-connected-map :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B} 
  is-connected-map neg-one-𝕋 f  is-surjective f
is-surjective-is-neg-one-connected-map H b = center (H b)
```

### A (k+1)-connected map is surjective

```agda
is-surjective-is-connected-map :
  {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2}
  {f : A  B}  is-connected-map (succ-𝕋 k) f 
  is-surjective f
is-surjective-is-connected-map neg-two-𝕋 H =
  is-surjective-is-neg-one-connected-map H
is-surjective-is-connected-map (succ-𝕋 k) H =
  is-surjective-is-connected-map
    ( k)
    ( is-connected-map-is-connected-map-succ-𝕋
      ( succ-𝕋 k)
      ( H))
```

### Precomposing functions into a family of `k+1`-types by a surjective map is a `k`-truncated map

```agda
is-trunc-map-precomp-Π-is-surjective :
  {l1 l2 l3 : Level} (k : 𝕋) 
  {A : UU l1} {B : UU l2} {f : A  B}  is-surjective f 
  (P : B  Truncated-Type l3 (succ-𝕋 k)) 
  is-trunc-map k (precomp-Π f  b  type-Truncated-Type (P b)))
is-trunc-map-precomp-Π-is-surjective k H =
  is-trunc-map-precomp-Π-is-connected-map
    ( neg-one-𝕋)
    ( succ-𝕋 k)
    ( k)
    ( refl)
    ( is-neg-one-connected-map-is-surjective H)
```

### Characterization of the identity type of `A ↠ B`

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

  htpy-surjection : (A  B)  UU (l1  l2)
  htpy-surjection g = map-surjection f ~ map-surjection g

  refl-htpy-surjection : htpy-surjection f
  refl-htpy-surjection = refl-htpy

  is-torsorial-htpy-surjection : is-torsorial htpy-surjection
  is-torsorial-htpy-surjection =
    is-torsorial-Eq-subtype
      ( is-torsorial-htpy (map-surjection f))
      ( is-prop-is-surjective)
      ( map-surjection f)
      ( refl-htpy)
      ( is-surjective-map-surjection f)

  htpy-eq-surjection :
    (g : A  B)  (f  g)  htpy-surjection g
  htpy-eq-surjection .f refl = refl-htpy-surjection

  is-equiv-htpy-eq-surjection :
    (g : A  B)  is-equiv (htpy-eq-surjection g)
  is-equiv-htpy-eq-surjection =
    fundamental-theorem-id is-torsorial-htpy-surjection htpy-eq-surjection

  extensionality-surjection :
    (g : A  B)  (f  g)  htpy-surjection g
  pr1 (extensionality-surjection g) = htpy-eq-surjection g
  pr2 (extensionality-surjection g) = is-equiv-htpy-eq-surjection g

  eq-htpy-surjection : (g : A  B)  htpy-surjection g  f  g
  eq-htpy-surjection g =
    map-inv-equiv (extensionality-surjection g)
```

### Characterization of the identity type of `Surjection l2 A`

```agda
equiv-Surjection :
  {l1 l2 l3 : Level} {A : UU l1} 
  Surjection l2 A  Surjection l3 A  UU (l1  l2  l3)
equiv-Surjection f g =
  Σ ( type-Surjection f  type-Surjection g)
    ( λ e  (map-equiv e  map-Surjection f) ~ map-Surjection g)

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

  id-equiv-Surjection : equiv-Surjection f f
  pr1 id-equiv-Surjection = id-equiv
  pr2 id-equiv-Surjection = refl-htpy

  is-torsorial-equiv-Surjection :
    is-torsorial (equiv-Surjection f)
  is-torsorial-equiv-Surjection =
    is-torsorial-Eq-structure
      ( λ Y g e  (map-equiv e  map-Surjection f) ~ map-surjection g)
      ( is-torsorial-equiv (type-Surjection f))
      ( type-Surjection f , id-equiv)
      ( is-torsorial-htpy-surjection (surjection-Surjection f))

  equiv-eq-Surjection :
    (g : Surjection l2 A)  (f  g)  equiv-Surjection f g
  equiv-eq-Surjection .f refl = id-equiv-Surjection

  is-equiv-equiv-eq-Surjection :
    (g : Surjection l2 A)  is-equiv (equiv-eq-Surjection g)
  is-equiv-equiv-eq-Surjection =
    fundamental-theorem-id
      is-torsorial-equiv-Surjection
      equiv-eq-Surjection

  extensionality-Surjection :
    (g : Surjection l2 A)  (f  g)  equiv-Surjection f g
  pr1 (extensionality-Surjection g) = equiv-eq-Surjection g
  pr2 (extensionality-Surjection g) = is-equiv-equiv-eq-Surjection g

  eq-equiv-Surjection :
    (g : Surjection l2 A)  equiv-Surjection f g  f  g
  eq-equiv-Surjection g = map-inv-equiv (extensionality-Surjection g)
```

### Characterization of the identity type of `Surjection-Into-Truncated-Type l2 k A`

```agda
equiv-Surjection-Into-Truncated-Type :
  {l1 l2 l3 : Level} {k : 𝕋} {A : UU l1} 
  Surjection-Into-Truncated-Type l2 k A 
  Surjection-Into-Truncated-Type l3 k A  UU (l1  l2  l3)
equiv-Surjection-Into-Truncated-Type f g =
  equiv-Surjection
    ( inclusion-Surjection-Into-Truncated-Type f)
    ( inclusion-Surjection-Into-Truncated-Type g)

module _
  {l1 l2 : Level} {k : 𝕋} {A : UU l1}
  (f : Surjection-Into-Truncated-Type l2 k A)
  where

  id-equiv-Surjection-Into-Truncated-Type :
    equiv-Surjection-Into-Truncated-Type f f
  id-equiv-Surjection-Into-Truncated-Type =
    id-equiv-Surjection (inclusion-Surjection-Into-Truncated-Type f)

  extensionality-Surjection-Into-Truncated-Type :
    (g : Surjection-Into-Truncated-Type l2 k A) 
    (f  g)  equiv-Surjection-Into-Truncated-Type f g
  extensionality-Surjection-Into-Truncated-Type g =
    ( extensionality-Surjection
      ( inclusion-Surjection-Into-Truncated-Type f)
      ( inclusion-Surjection-Into-Truncated-Type g)) ∘e
    ( equiv-ap-emb (emb-inclusion-Surjection-Into-Truncated-Type l2 k A))

  equiv-eq-Surjection-Into-Truncated-Type :
    (g : Surjection-Into-Truncated-Type l2 k A) 
    (f  g)  equiv-Surjection-Into-Truncated-Type f g
  equiv-eq-Surjection-Into-Truncated-Type g =
    map-equiv (extensionality-Surjection-Into-Truncated-Type g)

  refl-equiv-eq-Surjection-Into-Truncated-Type :
    equiv-eq-Surjection-Into-Truncated-Type f refl 
    id-equiv-Surjection-Into-Truncated-Type
  refl-equiv-eq-Surjection-Into-Truncated-Type = refl

  eq-equiv-Surjection-Into-Truncated-Type :
    (g : Surjection-Into-Truncated-Type l2 k A) 
    equiv-Surjection-Into-Truncated-Type f g  f  g
  eq-equiv-Surjection-Into-Truncated-Type g =
    map-inv-equiv (extensionality-Surjection-Into-Truncated-Type g)
```

### The type `Surjection-Into-Truncated-Type l2 (succ-𝕋 k) A` is `k`-truncated

This remains to be shown.
[#735](https://github.com/UniMath/agda-unimath/issues/735)

### Characterization of the identity type of `Surjection-Into-Set l2 A`

```agda
equiv-Surjection-Into-Set :
  {l1 l2 l3 : Level} {A : UU l1}  Surjection-Into-Set l2 A 
  Surjection-Into-Set l3 A  UU (l1  l2  l3)
equiv-Surjection-Into-Set = equiv-Surjection-Into-Truncated-Type

id-equiv-Surjection-Into-Set :
  {l1 l2 : Level} {A : UU l1} (f : Surjection-Into-Set l2 A) 
  equiv-Surjection-Into-Set f f
id-equiv-Surjection-Into-Set = id-equiv-Surjection-Into-Truncated-Type

extensionality-Surjection-Into-Set :
  {l1 l2 : Level} {A : UU l1} (f g : Surjection-Into-Set l2 A) 
  (f  g)  equiv-Surjection-Into-Set f g
extensionality-Surjection-Into-Set =
  extensionality-Surjection-Into-Truncated-Type

equiv-eq-Surjection-Into-Set :
  {l1 l2 : Level} {A : UU l1} (f g : Surjection-Into-Set l2 A) 
  (f  g)  equiv-Surjection-Into-Set f g
equiv-eq-Surjection-Into-Set = equiv-eq-Surjection-Into-Truncated-Type

refl-equiv-eq-Surjection-Into-Set :
  {l1 l2 : Level} {A : UU l1} (f : Surjection-Into-Set l2 A) 
  equiv-eq-Surjection-Into-Set f f refl 
  id-equiv-Surjection-Into-Set f
refl-equiv-eq-Surjection-Into-Set = refl-equiv-eq-Surjection-Into-Truncated-Type

eq-equiv-Surjection-Into-Set :
  {l1 l2 : Level} {A : UU l1} (f g : Surjection-Into-Set l2 A) 
  equiv-Surjection-Into-Set f g  f  g
eq-equiv-Surjection-Into-Set = eq-equiv-Surjection-Into-Truncated-Type
```

### Postcomposition of extensions along surjective maps by an embedding is an equivalence

```agda
module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
  where

  is-surjective-postcomp-extension-surjective-map :
    (f : A  B) (i : A  X) (g : X  Y) 
    is-surjective f  is-emb g 
    is-surjective (postcomp-extension f i g)
  is-surjective-postcomp-extension-surjective-map f i g H K (h , L) =
    unit-trunc-Prop
      ( ( j , N) ,
        ( eq-htpy-extension f
          ( g  i)
          ( postcomp-extension f i g (j , N))
          ( h , L)
          ( M)
          ( λ a 
            ( ap
              ( concat' (g (i a)) (M (f a)))
              ( is-section-map-inv-is-equiv
                ( K (i a) (j (f a)))
                ( L a  inv (M (f a))))) 
            ( is-section-inv-concat' (g (i a)) (M (f a)) (L a)))))
    where

    J : (b : B)  fiber g (h b)
    J =
      apply-dependent-universal-property-surj-is-surjective f H
        ( λ b  fiber-emb-Prop (g , K) (h b))
        ( λ a  (i a , L a))

    j : B  X
    j b = pr1 (J b)

    M : (g  j) ~ h
    M b = pr2 (J b)

    N : i ~ (j  f)
    N a = map-inv-is-equiv (K (i a) (j (f a))) (L a  inv (M (f a)))

  is-equiv-postcomp-extension-is-surjective :
    (f : A  B) (i : A  X) (g : X  Y) 
    is-surjective f  is-emb g 
    is-equiv (postcomp-extension f i g)
  is-equiv-postcomp-extension-is-surjective f i g H K =
    is-equiv-is-emb-is-surjective
      ( is-surjective-postcomp-extension-surjective-map f i g H K)
      ( is-emb-postcomp-extension f i g K)

  equiv-postcomp-extension-surjection :
    (f : A  B) (i : A  X) (g : X  Y) 
    extension (map-surjection f) i 
    extension (map-surjection f) (map-emb g  i)
  pr1 (equiv-postcomp-extension-surjection f i g) =
    postcomp-extension (map-surjection f) i (map-emb g)
  pr2 (equiv-postcomp-extension-surjection f i g) =
    is-equiv-postcomp-extension-is-surjective
      ( map-surjection f)
      ( i)
      ( map-emb g)
      ( is-surjective-map-surjection f)
      ( is-emb-map-emb g)
```

### Maps from the domain of a surjection into a set

```agda
module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A  B)
  (C : Set l3) (g : A  type-Set C) where

  is-prop-surj-comm-map-into-set :
    is-prop (Σ (B  type-Set C)  h  g ~ (h  map-surjection f)))
  is-prop-surj-comm-map-into-set =
    is-prop-all-elements-equal
       (h , q) (h' , q') 
        eq-type-subtype
          ( λ h''  Π-Prop A  a  Id-Prop C (g a) (h'' (map-surjection f a))))
          ( eq-htpy
            ( apply-dependent-universal-property-surjection
                ( f)
                ( λ b  Id-Prop C (h b) (h' b))
                ( λ a  inv (q a)  q' a))))

  map-universal-property-surj-into-set :
    Σ (B  type-Set C)  h  g ~ (h  map-surjection f)) 
    ((a a' : A)  map-surjection f a  map-surjection f a'  g a  g a')
  map-universal-property-surj-into-set (h , q) a a' p =
    q a  (ap h p  inv (q a'))

  inv-universal-property-surj-into-set :
    ((a a' : A)  map-surjection f a  map-surjection f a'  g a  g a') 
    Σ (B  type-Set C)  h  g ~ (h  map-surjection f))
  inv-universal-property-surj-into-set H =
    map-equiv
      ( e)
      (apply-dependent-universal-property-surjection
        ( f)
        ( λ b  P b , is-prop-P b)
        ( λ a  (g a , λ (a' , p')  H a' a p')))
    where
      P : B  UU (l1  l2  l3)
      P b =
        Σ (type-Set C)  c  (s : fiber (map-surjection f) b)  g (pr1 s)  c)

      e : ((b : B)  P b) 
          Σ (B  type-Set C)  h  g ~ (h  map-surjection f))
      e =
        (equiv-tot
           h 
            equiv-precomp-Π (inv-equiv-total-fiber (map-surjection f)) _)) ∘e
        (equiv-tot  h  inv-equiv equiv-ev-pair) ∘e
        (distributive-Π-Σ))

      is-prop-P : (b : B)  is-prop (P b)
      is-prop-P b =
        is-prop-all-elements-equal
          ( λ (pair c q) (pair c' q') 
            eq-type-subtype
              ( λ c'' 
                Π-Prop
                  (fiber (map-surjection f) b)
                   s  Id-Prop C (g (pr1 s)) c''))
              ( map-universal-property-trunc-Prop
                ( Id-Prop C c c')
                ( λ s  inv (q s)  q' s)
                ( is-surjective-map-surjection f b)))

  equiv-universal-property-surj-into-set :
    Σ (B  type-Set C)  h  g ~ (h  map-surjection f)) 
    ((a a' : A)  map-surjection f a  map-surjection f a'  g a  g a')
  pr1 equiv-universal-property-surj-into-set =
    map-universal-property-surj-into-set
  pr2 equiv-universal-property-surj-into-set =
    is-equiv-is-prop
      ( is-prop-surj-comm-map-into-set)
      ( is-prop-Π
         a 
          is-prop-Π
             a'  is-prop-function-type (is-set-type-Set C (g a) (g a')))))
      ( inv-universal-property-surj-into-set)

  function-inv-universal-property-surj-into-set :
    ((a a' : A)  map-surjection f a  map-surjection f a'  g a  g a') 
    B  type-Set C
  function-inv-universal-property-surj-into-set =
    pr1  map-inv-equiv equiv-universal-property-surj-into-set

  comm-inv-universal-property-surj-into-set :
    (H : (a a' : A)  map-surjection f a  map-surjection f a'  g a  g a') 
    g ~ (function-inv-universal-property-surj-into-set H  map-surjection f)
  comm-inv-universal-property-surj-into-set =
    pr2  map-inv-equiv equiv-universal-property-surj-into-set
```

### The type of surjections `A ↠ B` is equivalent to the type of families `P` of inhabited types over `B` equipped with an equivalence `A ≃ Σ B P`

This remains to be shown.
[#735](https://github.com/UniMath/agda-unimath/issues/735)

## See also

- In
  [Epimorphisms with respect to sets](foundation.epimorphisms-with-respect-to-sets.md)
  we show that a map is surjective if and only if it is an epimorphism with
  respect to sets.