Fibers of maps

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

Created on 2022-01-26.
Last modified on 2024-03-02.

module foundation.fibers-of-maps where

open import foundation-core.fibers-of-maps public
Imports 
open import foundation.action-on-identifications-functions
open import foundation.cones-over-cospan-diagrams
open import foundation.dependent-pair-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.type-arithmetic-unit-type
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.pullbacks
open import foundation-core.transport-along-identifications
open import foundation-core.universal-property-pullbacks

Properties

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

  square-fiber :
    f ∘ pr1 ~ point b ∘ terminal-map (fiber f b)
  square-fiber = pr2

  cone-fiber : cone f (point b) (fiber f b)
  pr1 cone-fiber = pr1
  pr1 (pr2 cone-fiber) = terminal-map (fiber f b)
  pr2 (pr2 cone-fiber) = square-fiber

  abstract
    is-pullback-cone-fiber : is-pullback f (point b) cone-fiber
    is-pullback-cone-fiber =
      is-equiv-tot-is-fiberwise-equiv
        ( λ a → is-equiv-map-inv-left-unit-law-product)

  abstract
    universal-property-pullback-cone-fiber :
      universal-property-pullback f (point b) cone-fiber
    universal-property-pullback-cone-fiber =
      universal-property-pullback-is-pullback f
        ( point b)
        ( cone-fiber)
        ( is-pullback-cone-fiber)

The fiber of the terminal map at any point is equivalent to its domain

module _
  {l : Level} {A : UU l}
  where

  equiv-fiber-terminal-map :
    (u : unit) → fiber (terminal-map A) u ≃ A
  equiv-fiber-terminal-map u =
    right-unit-law-Σ-is-contr
      ( λ a → is-prop-unit (terminal-map A a) u)

  inv-equiv-fiber-terminal-map :
    (u : unit) → A ≃ fiber (terminal-map A) u
  inv-equiv-fiber-terminal-map u =
    inv-equiv (equiv-fiber-terminal-map u)

  equiv-fiber-terminal-map-star :
    fiber (terminal-map A) star ≃ A
  equiv-fiber-terminal-map-star = equiv-fiber-terminal-map star

  inv-equiv-fiber-terminal-map-star :
    A ≃ fiber (terminal-map A) star
  inv-equiv-fiber-terminal-map-star =
    inv-equiv equiv-fiber-terminal-map-star

The total space of the fibers of the terminal map is equivalent to its domain

module _
  {l : Level} {A : UU l}
  where

  equiv-total-fiber-terminal-map :
    Σ unit (fiber (terminal-map A)) ≃ A
  equiv-total-fiber-terminal-map =
    ( left-unit-law-Σ-is-contr is-contr-unit star) ∘e
    ( equiv-tot equiv-fiber-terminal-map)

  inv-equiv-total-fiber-terminal-map :
    A ≃ Σ unit (fiber (terminal-map A))
  inv-equiv-total-fiber-terminal-map =
    inv-equiv equiv-total-fiber-terminal-map

Transport in fibers

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

  compute-tr-fiber :
    {y y' : B} (p : y ＝ y') (u : fiber f y) →
    tot (λ x → concat' _ p) u ＝ tr (fiber f) p u
  compute-tr-fiber refl u = ap (pair _) right-unit

Table of files about fibers of maps

The following table lists files that are about fibers of maps as a general concept.

ConceptFile
Fibers of maps (foundation-core)foundation-core.fibers-of-maps
Fibers of maps (foundation)foundation.fibers-of-maps
Equality in the fibers of a mapfoundation.equality-fibers-of-maps
Functoriality of fibers of mapsfoundation.functoriality-fibers-of-maps
Fibers of pointed mapsstructured-types.fibers-of-pointed-maps
Fibers of maps of finite typesunivalent-combinatorics.fibers-of-maps
The universal property of the family of fibers of mapsfoundation.universal-property-family-of-fibers-of-maps

Recent changes