0-Images of maps

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-07-18.
Last modified on 2024-08-22.

module foundation.0-images-of-maps where
Imports 
open import foundation.truncation-images-of-maps
open import foundation.universe-levels

open import foundation-core.truncation-levels

Idea

The 0-image of a map f : A → B is the type

  0-im f := Σ (b : B), type-trunc-Set (fiber f b).

The map A → 0-im f is 0-connected and the map 0-im f → B is 0-truncated.

Definition

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

  0-im : UU (l1 ⊔ l2)
  0-im = trunc-im zero-𝕋 f

  unit-0-im : A → 0-im
  unit-0-im = unit-trunc-im zero-𝕋 f

  projection-0-im : 0-im → B
  projection-0-im = projection-trunc-im zero-𝕋 f

Properties

Characterization of the identity type of 0-im f

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

  Eq-unit-0-im : A → A → UU (l1 ⊔ l2)
  Eq-unit-0-im = Eq-unit-trunc-im neg-one-𝕋 f

Recent changes