Truncation images of maps

module foundation.truncation-images-of-maps where

Imports

open import foundation.truncations

open import foundation-core.dependent-pair-types
open import foundation-core.fibers-of-maps
open import foundation-core.identity-types
open import foundation-core.truncation-levels
open import foundation-core.universe-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 (fib 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 (fib 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 →
        {!!})) ∘e
    ( equiv-pair-eq-Σ
      ( unit-trunc-im (succ-𝕋 k) f x)
      ( unit-trunc-im (succ-𝕋 k) f y))
-}