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

Created on 2022-01-27.
Last modified on 2024-01-14.

module foundation.0-maps where
open import foundation.dependent-pair-types
open import foundation.functoriality-dependent-pair-types
open import foundation.universe-levels

open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.sets
open import foundation-core.truncated-maps
open import foundation-core.truncation-levels


Maps f : A → B of which the fibers are sets, i.e., 0-truncated types, are called 0-maps. It is shown in foundation.faithful-maps that a map f is a 0-map if and only if f is faithful, i.e., f induces embeddings on identity types.

module _
  {l1 l2 : Level}

  is-0-map : {A : UU l1} {B : UU l2}  (A  B)  UU (l1  l2)
  is-0-map {A} {B} f = (y : B)  is-set (fiber f y)

  0-map : (A : UU l1) (B : UU l2)  UU (l1  l2)
  0-map A B = Σ (A  B) is-0-map

  map-0-map : {A : UU l1} {B : UU l2}  0-map A B  A  B
  map-0-map = pr1

  is-0-map-map-0-map :
    {A : UU l1} {B : UU l2} (f : 0-map A B)  is-0-map (map-0-map f)
  is-0-map-map-0-map = pr2


Projections of families of sets are 0-maps

module _
  {l1 l2 : Level} {A : UU l1}

    is-0-map-pr1 :
      {B : A  UU l2}  ((x : A)  is-set (B x))  is-0-map (pr1 {B = B})
    is-0-map-pr1 {B} H x =
      is-set-equiv (B x) (equiv-fiber-pr1 B x) (H x)

  pr1-0-map :
    (B : A  Set l2)  0-map (Σ A  x  type-Set (B x))) A
  pr1 (pr1-0-map B) = pr1
  pr2 (pr1-0-map B) = is-0-map-pr1  x  is-set-type-Set (B x))

0-maps are closed under homotopies

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f g : A  B} (H : f ~ g)

  is-0-map-htpy : is-0-map g  is-0-map f
  is-0-map-htpy = is-trunc-map-htpy zero-𝕋 H

0-maps are closed under composition

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

  is-0-map-comp :
    (g : B  X) (h : A  B) 
    is-0-map g  is-0-map h  is-0-map (g  h)
  is-0-map-comp = is-trunc-map-comp zero-𝕋

  is-0-map-left-map-triangle :
    (f : A  X) (g : B  X) (h : A  B) (H : f ~ (g  h)) 
    is-0-map g  is-0-map h  is-0-map f
  is-0-map-left-map-triangle = is-trunc-map-left-map-triangle zero-𝕋

If a composite is a 0-map, then so is its right factor

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

  is-0-map-right-factor :
    (g : B  X) (h : A  B) 
    is-0-map g  is-0-map (g  h)  is-0-map h
  is-0-map-right-factor = is-trunc-map-right-factor zero-𝕋

  is-0-map-top-map-triangle :
    (f : A  X) (g : B  X) (h : A  B) (H : f ~ (g  h)) 
    is-0-map g  is-0-map f  is-0-map h
  is-0-map-top-map-triangle = is-trunc-map-top-map-triangle zero-𝕋

Families of 0-maps induce 0-maps on total spaces

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A  UU l2} {C : A  UU l3}
  {f : (x : A)  B x  C x}

    is-0-map-tot : ((x : A)  is-0-map (f x))  is-0-map (tot f)
    is-0-map-tot = is-trunc-map-tot zero-𝕋

For any type family over the codomain, a 0-map induces a 0-map on total spaces

In other words, 0-maps are stable under pullbacks. We will come to this point when we introduce homotopy pullbacks.

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {f : A  B} (C : B  UU l3)

    is-0-map-map-Σ-map-base : is-0-map f  is-0-map (map-Σ-map-base f C)
    is-0-map-map-Σ-map-base = is-trunc-map-map-Σ-map-base zero-𝕋 C

The functorial action of Σ preserves 0-maps

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : A  UU l3}
  (D : B  UU l4) {f : A  B} {g : (x : A)  C x  D (f x)}

  is-0-map-map-Σ :
    is-0-map f  ((x : A)  is-0-map (g x))  is-0-map (map-Σ D f g)
  is-0-map-map-Σ = is-trunc-map-map-Σ zero-𝕋 D

Recent changes