Surjective maps

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Victor Blanchi, Elisabeth Stenholm, Gregor Perčič, Daniel Gratzer, Elif Uskuplu, Håkon Gylterud and Raymond Baker.

Created on 2022-02-09.
Last modified on 2024-02-06.

module foundation.surjective-maps where
Imports
open import foundation.action-on-identifications-functions
open import foundation.connected-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equality-cartesian-product-types
open import foundation.functoriality-cartesian-product-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopy-induction
open import foundation.identity-types
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.truncated-types
open import foundation.univalence
open import foundation.universal-property-family-of-fibers-of-maps
open import foundation.universal-property-propositional-truncation
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
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.homotopies
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.subtypes
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

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

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} 
    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

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

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

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

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

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))))
        ( universal-property-family-of-fibers-fiber f (is-in-subtype P))

  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

abstract
  is-surjective-is-propositional-truncation :
    {l1 l2 : Level} {A : UU l1} {P : Prop l2} (f : A  type-Prop P) 
    dependent-universal-property-propositional-truncation 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 
    dependent-universal-property-propositional-truncation 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)
            ( fiber-emb-Prop (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-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

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

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

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

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

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

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

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

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
      ( 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

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

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

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

See also

Recent changes