Truncation images of maps

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Daniel Gratzer and Elisabeth Stenholm.

Created on 2022-07-19.
Last modified on 2023-12-21.

module foundation.truncation-images-of-maps where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.connected-maps
open import foundation.dependent-pair-types
open import foundation.fibers-of-maps
open import foundation.functoriality-truncation
open import foundation.identity-types
open import foundation.truncations
open import foundation.universe-levels

open import foundation-core.equality-dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.transport-along-identifications
open import foundation-core.truncated-maps
open import foundation-core.truncation-levels

Idea

The k-truncation image of a map f : A → B is the type trunc-im k f that fits in the (k-connected,k-truncated) factorization of f. It is defined as the type

  trunc-im k f := Σ (y : B), type-trunc k (fiber f y)

Definition

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

  trunc-im : UU (l1 ⊔ l2)
  trunc-im = Σ B (λ y → type-trunc k (fiber f y))

  unit-trunc-im : A → trunc-im
  pr1 (unit-trunc-im x) = f x
  pr2 (unit-trunc-im x) = unit-trunc (pair x refl)

  projection-trunc-im : trunc-im → B
  projection-trunc-im = pr1

Properties

Characterization of the identity types of k+1-truncation images

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

  Eq-unit-trunc-im : A → A → UU (l1 ⊔ l2)
  Eq-unit-trunc-im x y = trunc-im k (ap f {x} {y})

  extensionality-trunc-im :
    (x y : A) →
    ( unit-trunc-im (succ-𝕋 k) f x ＝ unit-trunc-im (succ-𝕋 k) f y) ≃
    ( Eq-unit-trunc-im x y)
  extensionality-trunc-im x y =
    ( equiv-tot
      ( λ q →
        ( equiv-trunc k
          ( ( equiv-tot
              ( λ p → equiv-concat (inv right-unit) q)) ∘e
            ( equiv-Eq-eq-fiber f (f y)))) ∘e
        ( inv-equiv (effectiveness-trunc k (x , q) (y , refl))) ∘e
        ( equiv-concat
          ( ap unit-trunc (compute-tr-fiber f q (x , refl)))
          ( unit-trunc (y , refl))) ∘e
        ( equiv-concat
          ( preserves-tr (λ _ → unit-trunc) q (x , refl))
          ( unit-trunc (y , refl))))) ∘e
    ( equiv-pair-eq-Σ
      ( unit-trunc-im (succ-𝕋 k) f x)
      ( unit-trunc-im (succ-𝕋 k) f y))

The map projection-trunc-im k is k-truncated

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

  is-trunc-map-projection-trunc-im : is-trunc-map k (projection-trunc-im k f)
  is-trunc-map-projection-trunc-im =
    is-trunc-map-pr1 k (λ _ → is-trunc-type-trunc)

The map unit-trunc-im k is k-connected

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

  is-connected-map-unit-trunc-im : is-connected-map k (unit-trunc-im k f)
  is-connected-map-unit-trunc-im =
    is-connected-map-comp k
      ( is-connected-map-tot-is-fiberwise-connected-map k
        ( λ b → unit-trunc)
        ( λ b → is-connected-map-unit-trunc k))
      ( is-connected-map-is-equiv (is-equiv-map-inv-equiv-total-fiber f))

Recent changes