Surjective maps

module foundation.surjective-maps where
Imports
open import foundation.connected-maps
open import foundation.contractible-types
open import foundation.embeddings
open import foundation.functoriality-cartesian-product-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.structure-identity-principle
open import foundation.truncated-types
open import foundation.univalence
open import foundation.universal-property-propositional-truncation

open import foundation-core.constant-maps
open import foundation-core.contractible-maps
open import foundation-core.dependent-pair-types
open import foundation-core.equality-cartesian-product-types
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.functions
open import foundation-core.functoriality-dependent-function-types
open import foundation-core.fundamental-theorem-of-identity-types
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.subtype-identity-principle
open import foundation-core.truncated-maps
open import foundation-core.truncation-levels
open import foundation-core.universe-levels

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

Idea

A map f : A → B is surjective if all of its fibers are inhabited.

Definition

Surjective maps

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  fib 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)

_↠_ : {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

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

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

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

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

Any equivalence is surjective

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 dependent universal property of surjective maps

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

abstract
  is-surjective-dependent-universal-property-surj :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
    ({l : Level}  dependent-universal-property-surj l f) 
    is-surjective f
  is-surjective-dependent-universal-property-surj f dup-surj-f =
    map-inv-is-equiv
      ( dup-surj-f  b  trunc-Prop (fib f b)))
      ( λ x  unit-trunc-Prop (pair x refl))

abstract
  square-dependent-universal-property-surj :
    {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
    (P : B  Prop l3) 
    ( λ (h : (y : B)  type-Prop (P y)) x  h (f x)) ~
    ( ( λ h x  h (f x) (pair x refl)) 
      ( ( λ h y  (h y)  unit-trunc-Prop) 
        ( λ h y  const (type-trunc-Prop (fib f y)) (type-Prop (P y)) (h y))))
  square-dependent-universal-property-surj f P = refl-htpy

  dependent-universal-property-surj-is-surjective :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
    is-surjective f 
    ({l : Level}  dependent-universal-property-surj l f)
  dependent-universal-property-surj-is-surjective f is-surj-f P =
    is-equiv-comp
      ( λ h x  h (f x) (pair x refl))
      ( ( λ h y  (h y)  unit-trunc-Prop) 
        ( λ h y  const (type-trunc-Prop (fib f y)) (type-Prop (P y)) (h y)))
      ( is-equiv-comp
        ( λ h y  (h y)  unit-trunc-Prop)
        ( λ h y  const (type-trunc-Prop (fib f y)) (type-Prop (P y)) (h y))
        ( is-equiv-map-Π
          ( λ y p z  p)
          ( λ 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-Π
          ( λ b g  g  unit-trunc-Prop)
          ( λ b  is-propositional-truncation-trunc-Prop (fib f b) (P b))))
      ( is-equiv-map-reduce-Π-fib f ( λ y z  type-Prop (P y)))

equiv-dependent-universal-property-surj-is-surjective :
  {l l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
  is-surjective f  (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 f H C) h x = h (f x)
pr2 (equiv-dependent-universal-property-surj-is-surjective f H C) =
  dependent-universal-property-surj-is-surjective f H C

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

apply-twice-dependent-universal-property-surj-is-surjective :
  {l l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
  is-surjective f  (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 f H C G s =
  apply-dependent-universal-property-surj-is-surjective
    ( f)
    ( H)
    ( λ b  C s b)
    ( λ y 
      apply-dependent-universal-property-surj-is-surjective
        ( f)
        ( H)
        ( λ b  C b (f y))
         x  G x y)
        ( s))

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

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

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)
            ( fib-emb-Prop (pair f K) y)
            ( id)))

The composite of surjective maps is surjective

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

  abstract
    is-surjective-comp-htpy :
      (f : A  X) (g : B  X) (h : A  B) (H : f ~ (g  h)) 
      is-surjective g  is-surjective h  is-surjective f
    is-surjective-comp-htpy f g h H is-surj-g is-surj-h x =
      apply-universal-property-trunc-Prop
        ( is-surj-g x)
        ( trunc-Prop (fib f x))
        ( λ { (pair b refl) 
          apply-universal-property-trunc-Prop
            ( is-surj-h b)
            ( trunc-Prop (fib f (g b)))
            ( λ { (pair a refl) 
              unit-trunc-Prop (pair 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-comp-htpy (g  h) g h refl-htpy

Functoriality of products preserves being surjective

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 (fib (map-prod f g) (c , d)))
      ( λ x y 
        unit-trunc-Prop
          ( pair
            ( (pr1 x) , (pr1 y))
            ( eq-pair (pr2 x) (pr2 y))))

The composite of a surjective map with an equivalence is surjective

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

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

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

  abstract
    is-surjective-left-factor-htpy :
      (f : A  X) (g : B  X) (h : A  B) (H : f ~ (g  h)) 
      is-surjective f  is-surjective g
    is-surjective-left-factor-htpy f g h H is-surj-f x =
      apply-universal-property-trunc-Prop
        ( is-surj-f x)
        ( trunc-Prop (fib g x))
        ( λ { (pair a refl) 
          unit-trunc-Prop (pair (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-left-factor-htpy (g  h) g h refl-htpy

Surjective maps are -1-connected

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)

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

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

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-contr-total-htpy-surjection : is-contr (Σ (A  B) htpy-surjection)
  is-contr-total-htpy-surjection =
    is-contr-total-Eq-subtype
      ( is-contr-total-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-contr-total-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

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-contr-total-equiv-Surjection :
    is-contr (Σ (Surjection l2 A) (equiv-Surjection f))
  is-contr-total-equiv-Surjection =
    is-contr-total-Eq-structure
      ( λ Y g e  (map-equiv e  map-Surjection f) ~ map-surjection g)
      ( is-contr-total-equiv (type-Surjection f))
      ( pair (type-Surjection f) id-equiv)
      ( is-contr-total-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-contr-total-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

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.

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

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

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)))
              ( issec-map-inv-is-equiv
                ( K (i a) ((j (f a))))
                ( L a  inv (M (f a))))) 
            ( issec-inv-concat' (g (i a)) (M (f a)) (L a)))))
    where

    J : (b : B)  fib g (h b)
    J =
      apply-dependent-universal-property-surj-is-surjective f H
        ( λ b  fib-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)

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