0-Maps

module foundation-core.0-maps where

Imports

open import foundation-core.dependent-pair-types
open import foundation-core.fibers-of-maps
open import foundation-core.functions
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.sets
open import foundation-core.truncated-maps
open import foundation-core.truncation-levels
open import foundation-core.universe-levels

Definition

Maps f : A → B of which the fibers are sets, i.e., 0-truncated types, are called 0-maps. We will show in foundation-core.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}
  where

  is-0-map : {A : UU l1} {B : UU l2} → (A → B) → UU (l1 ⊔ l2)
  is-0-map {A} {B} f = (y : B) → is-set (fib 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

Properties

Projections of families of sets are `0`-maps

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

  abstract
    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-fib-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)
  where

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

  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-comp-htpy :
    (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-comp-htpy = is-trunc-map-comp-htpy 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}
  where

  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-right-factor-htpy :
    (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-right-factor-htpy = is-trunc-map-right-factor-htpy zero-𝕋

A family of `0`-maps induces a `0`-map 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}
  where

  abstract
    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)
  where

  abstract
    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)}
  where

  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