The universal property of the family of fibers of maps

Content created by Fredrik Bakke, Egbert Rijke, Raymond Baker and Vojtěch Štěpančík.

Created on 2023-12-05.
Last modified on 2026-05-02.

module foundation.universal-property-family-of-fibers-of-maps where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences-contractible-types
open import foundation.families-of-equivalences
open import foundation.function-extensionality
open import foundation.function-extensionality-axiom
open import foundation.precomposition-dependent-functions
open import foundation.precomposition-functions
open import foundation.subtype-identity-principle
open import foundation.type-theoretic-principle-of-choice
open import foundation.universal-property-dependent-pair-types
open import foundation.universe-levels

open import foundation-core.contractible-maps
open import foundation-core.contractible-types
open import foundation-core.dependent-identifications
open import foundation-core.diagonal-maps-of-types
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-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.retractions
open import foundation-core.sections

open import orthogonal-factorization-systems.extensions-double-lifts-families-of-elements
open import orthogonal-factorization-systems.lifts-families-of-elements

Idea

Any map f : A → B induces a type family fiber f : B → 𝒰 of fibers of f. By precomposing with f, we obtain the type family (fiber f) ∘ f : A → 𝒰, which always has a section given by

  λ a → (a , refl) : (a : A) → fiber f (f a).

We can uniquely characterize the family of fibers fiber f : B → 𝒰 as the initial type family equipped with such a section. Explicitly, the universal property of the family of fibers fiber f : B → 𝒰 of a map f is that the precomposition operation

  ((b : B) → fiber f b → X b) → ((a : A) → X (f a))

is an equivalence for any type family X : B → 𝒰. Note that for any type family X over B and any map f : A → B, the type of lifts of f to X is precisely the type of sections

  (a : A) → X (f a).

The family of fibers of f is therefore the initial type family over B equipped with a lift of f.

This universal property is especially useful when A or B enjoy mapping out universal properties. This lets us characterize the sections (a : A) → X (f a) in terms of the mapping out properties of A and the descent data of B.

Note: We disambiguate between the universal property of the family of fibers of a map and the universal property of the fiber of a map at a point in the codomain. The universal property of the family of fibers of a map is as described above, while the universal property of the fiber fiber f b of a map f at b is a special case of the universal property of pullbacks.

Definitions

The dependent universal property of the family of fibers of a map

Consider a map f : A → B and a type family F : B → 𝒰 equipped with a lift δ : (a : A) → F (f a) of f to F. Then there is an evaluation map

  ((b : B) (z : F b) → X b z) → ((a : A) → X (f a) (δ a))

for any binary type family X : (b : B) → F b → 𝒰. This evaluation map takes a binary family of elements of X to a double lift of f and δ. The dependent universal property of the family of fibers of a map f asserts that this evaluation map is an equivalence.

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

  dependent-universal-property-family-of-fibers :
    {f : A → B} (F : B → UU l3) (δ : lift-family-of-elements F f) → UUω
  dependent-universal-property-family-of-fibers F δ =
    {l : Level} (X : (b : B) → F b → UU l) →
    is-equiv (ev-double-lift-family-of-elements {B = F} {X} δ)

The universal property of the family of fibers of a map

Consider a map f : A → B and a type family F : B → 𝒰 equipped with a lift δ : (a : A) → F (f a) of f to F. Then there is an evaluation map

  ((b : B) → F b → X b) → ((a : A) → X (f a))

for any binary type family X : B → 𝒰. This evaluation map takes a binary family of elements of X to a double lift of f and δ. The universal property of the family of fibers of f asserts that this evaluation map is an equivalence.

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

  universal-property-family-of-fibers :
    {f : A → B} (F : B → UU l3) (δ : lift-family-of-elements F f) → UUω
  universal-property-family-of-fibers F δ =
    {l : Level} (X : B → UU l) →
    is-equiv (ev-double-lift-family-of-elements {B = F} {λ b _ → X b} δ)

The lift of any map to its family of fibers

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

  lift-family-of-elements-fiber : lift-family-of-elements (fiber f) f
  pr1 (lift-family-of-elements-fiber a) = a
  pr2 (lift-family-of-elements-fiber a) = refl

  lift-family-of-elements-fiber' : lift-family-of-elements (fiber' f) f
  pr1 (lift-family-of-elements-fiber' a) = a
  pr2 (lift-family-of-elements-fiber' a) = refl

Properties

The family of fibers of a map satisfies the dependent universal property of the family of fibers of a map

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B)
  (C : (y : B) (z : fiber f y) → UU l3)
  where

  ev-lift-family-of-elements-fiber :
    ((y : B) (z : fiber f y) → C y z) → ((x : A) → C (f x) (x , refl))
  ev-lift-family-of-elements-fiber =
    ev-double-lift-family-of-elements (lift-family-of-elements-fiber f)

  extend-lift-family-of-elements-fiber :
    ((x : A) → C (f x) (x , refl)) → ((y : B) (z : fiber f y) → C y z)
  extend-lift-family-of-elements-fiber h .(f x) (x , refl) = h x

  is-section-extend-lift-family-of-elements-fiber :
    is-section
      ( ev-lift-family-of-elements-fiber)
      ( extend-lift-family-of-elements-fiber)
  is-section-extend-lift-family-of-elements-fiber h = refl

  htpy-is-retraction-extend-lift-family-of-elements-fiber :
    (h : (y : B) (z : fiber f y) → C y z) (y : B) →
    extend-lift-family-of-elements-fiber
      ( ev-lift-family-of-elements-fiber h)
      ( y) ~
    h y
  htpy-is-retraction-extend-lift-family-of-elements-fiber h .(f z) (z , refl) =
    refl

  abstract
    is-retraction-extend-lift-family-of-elements-fiber :
      is-retraction
        ( ev-lift-family-of-elements-fiber)
        ( extend-lift-family-of-elements-fiber)
    is-retraction-extend-lift-family-of-elements-fiber h =
      eq-htpy
        ( eq-htpy ∘ htpy-is-retraction-extend-lift-family-of-elements-fiber h)

  is-equiv-extend-lift-family-of-elements-fiber :
    is-equiv extend-lift-family-of-elements-fiber
  is-equiv-extend-lift-family-of-elements-fiber =
    is-equiv-is-invertible
      ( ev-lift-family-of-elements-fiber)
      ( is-retraction-extend-lift-family-of-elements-fiber)
      ( is-section-extend-lift-family-of-elements-fiber)

  inv-equiv-dependent-universal-property-family-of-fibers :
    ((x : A) → C (f x) (x , refl)) ≃ ((y : B) (z : fiber f y) → C y z)
  inv-equiv-dependent-universal-property-family-of-fibers =
    ( extend-lift-family-of-elements-fiber ,
      is-equiv-extend-lift-family-of-elements-fiber)

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

  dependent-universal-property-family-of-fibers-fiber :
    dependent-universal-property-family-of-fibers
      ( fiber f)
      ( lift-family-of-elements-fiber f)
  dependent-universal-property-family-of-fibers-fiber C =
    is-equiv-is-invertible
      ( extend-lift-family-of-elements-fiber f C)
      ( is-section-extend-lift-family-of-elements-fiber f C)
      ( is-retraction-extend-lift-family-of-elements-fiber f C)

  equiv-dependent-universal-property-family-of-fibers :
    {l3 : Level} (C : (y : B) (z : fiber f y) → UU l3) →
    ((y : B) (z : fiber f y) → C y z) ≃
    ((x : A) → C (f x) (x , refl))
  equiv-dependent-universal-property-family-of-fibers C =
    ( ev-lift-family-of-elements-fiber f C ,
      dependent-universal-property-family-of-fibers-fiber C)

The variant family of fibers of a map satisfies the dependent universal property of the family of fibers of a map

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B)
  (C : (y : B) (z : fiber' f y) → UU l3)
  where

  ev-lift-family-of-elements-fiber' :
    ((y : B) (z : fiber' f y) → C y z) → ((x : A) → C (f x) (x , refl))
  ev-lift-family-of-elements-fiber' =
    ev-double-lift-family-of-elements (lift-family-of-elements-fiber' f)

  extend-lift-family-of-elements-fiber' :
    ((x : A) → C (f x) (x , refl)) → ((y : B) (z : fiber' f y) → C y z)
  extend-lift-family-of-elements-fiber' h .(f x) (x , refl) = h x

  is-section-extend-lift-family-of-elements-fiber' :
    is-section
      ( ev-lift-family-of-elements-fiber')
      ( extend-lift-family-of-elements-fiber')
  is-section-extend-lift-family-of-elements-fiber' h = refl

  htpy-is-retraction-extend-lift-family-of-elements-fiber' :
    (h : (y : B) (z : fiber' f y) → C y z) (y : B) →
    extend-lift-family-of-elements-fiber'
      ( ev-lift-family-of-elements-fiber' h)
      ( y) ~
    h y
  htpy-is-retraction-extend-lift-family-of-elements-fiber' h .(f z) (z , refl) =
    refl

  abstract
    is-retraction-extend-lift-family-of-elements-fiber' :
      is-retraction
        ( ev-lift-family-of-elements-fiber')
        ( extend-lift-family-of-elements-fiber')
    is-retraction-extend-lift-family-of-elements-fiber' h =
      eq-htpy
        ( eq-htpy ∘ htpy-is-retraction-extend-lift-family-of-elements-fiber' h)

  is-equiv-extend-lift-family-of-elements-fiber' :
    is-equiv extend-lift-family-of-elements-fiber'
  is-equiv-extend-lift-family-of-elements-fiber' =
    is-equiv-is-invertible
      ( ev-lift-family-of-elements-fiber')
      ( is-retraction-extend-lift-family-of-elements-fiber')
      ( is-section-extend-lift-family-of-elements-fiber')

  inv-equiv-dependent-universal-property-family-of-fibers' :
    ((x : A) → C (f x) (x , refl)) ≃ ((y : B) (z : fiber' f y) → C y z)
  inv-equiv-dependent-universal-property-family-of-fibers' =
    ( extend-lift-family-of-elements-fiber' ,
      is-equiv-extend-lift-family-of-elements-fiber')

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

  dependent-universal-property-family-of-fibers-fiber' :
    dependent-universal-property-family-of-fibers
      ( fiber' f)
      ( lift-family-of-elements-fiber' f)
  dependent-universal-property-family-of-fibers-fiber' C =
    is-equiv-is-invertible
      ( extend-lift-family-of-elements-fiber' f C)
      ( is-section-extend-lift-family-of-elements-fiber' f C)
      ( is-retraction-extend-lift-family-of-elements-fiber' f C)

  equiv-dependent-universal-property-family-of-fibers' :
    {l3 : Level} (C : (y : B) (z : fiber' f y) → UU l3) →
    ((y : B) (z : fiber' f y) → C y z) ≃
    ((x : A) → C (f x) (x , refl))
  equiv-dependent-universal-property-family-of-fibers' C =
    ( ev-lift-family-of-elements-fiber' f C ,
      dependent-universal-property-family-of-fibers-fiber' C)

The family of fibers of a map satisfies the universal property of the family of fibers of a map

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

  universal-property-family-of-fibers-fiber :
    universal-property-family-of-fibers
      ( fiber f)
      ( lift-family-of-elements-fiber f)
  universal-property-family-of-fibers-fiber C =
    dependent-universal-property-family-of-fibers-fiber f (λ y _ → C y)

  equiv-universal-property-family-of-fibers :
    {l3 : Level} (C : B → UU l3) →
    ((y : B) → fiber f y → C y) ≃ lift-family-of-elements C f
  equiv-universal-property-family-of-fibers C =
    equiv-dependent-universal-property-family-of-fibers f (λ y _ → C y)

The inverse equivalence of the universal property of the family of fibers of a map

The inverse of the equivalence equiv-universal-property-family-of-fibers has a reasonably nice definition, so we also record it here.

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

  inv-equiv-universal-property-family-of-fibers :
    (lift-family-of-elements C f) ≃ ((y : B) → fiber f y → C y)
  inv-equiv-universal-property-family-of-fibers =
    inv-equiv-dependent-universal-property-family-of-fibers f (λ y _ → C y)

If a type family equipped with a lift of a map satisfies the universal property of the family of fibers, then it satisfies a unique extension property

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {f : A → B}
  {F : B → UU l3} {δ : (a : A) → F (f a)}
  (u : universal-property-family-of-fibers F δ)
  (G : B → UU l4) (γ : (a : A) → G (f a))
  where

  abstract
    uniqueness-extension-universal-property-family-of-fibers :
      is-contr
        ( extension-double-lift-family-of-elements (λ y (_ : F y) → G y) δ γ)
    uniqueness-extension-universal-property-family-of-fibers =
      is-contr-equiv
        ( fiber (ev-double-lift-family-of-elements δ) γ)
        ( equiv-tot (λ h → equiv-eq-htpy))
        ( is-contr-map-is-equiv (u G) γ)

  abstract
    extension-universal-property-family-of-fibers :
      extension-double-lift-family-of-elements (λ y (_ : F y) → G y) δ γ
    extension-universal-property-family-of-fibers =
      center uniqueness-extension-universal-property-family-of-fibers

  fiberwise-map-universal-property-family-of-fibers :
    (b : B) → F b → G b
  fiberwise-map-universal-property-family-of-fibers =
    family-of-elements-extension-double-lift-family-of-elements
      extension-universal-property-family-of-fibers

  is-extension-fiberwise-map-universal-property-family-of-fibers :
    is-extension-double-lift-family-of-elements
      ( λ y _ → G y)
      ( δ)
      ( γ)
      ( fiberwise-map-universal-property-family-of-fibers)
  is-extension-fiberwise-map-universal-property-family-of-fibers =
    is-extension-extension-double-lift-family-of-elements
      extension-universal-property-family-of-fibers

The family of fibers of a map is uniquely unique

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} (f : A → B) (F : B → UU l3)
  (δ : (a : A) → F (f a)) (u : universal-property-family-of-fibers F δ)
  (G : B → UU l4) (γ : (a : A) → G (f a))
  (v : universal-property-family-of-fibers G γ)
  where

  is-retraction-extension-universal-property-family-of-fibers :
    comp-extension-double-lift-family-of-elements
      ( extension-universal-property-family-of-fibers v F δ)
      ( extension-universal-property-family-of-fibers u G γ) ＝
    id-extension-double-lift-family-of-elements δ
  is-retraction-extension-universal-property-family-of-fibers =
    eq-is-contr
      ( uniqueness-extension-universal-property-family-of-fibers u F δ)

  is-section-extension-universal-property-family-of-fibers :
    comp-extension-double-lift-family-of-elements
      ( extension-universal-property-family-of-fibers u G γ)
      ( extension-universal-property-family-of-fibers v F δ) ＝
    id-extension-double-lift-family-of-elements γ
  is-section-extension-universal-property-family-of-fibers =
    eq-is-contr
      ( uniqueness-extension-universal-property-family-of-fibers v G γ)

  is-retraction-fiberwise-map-universal-property-family-of-fibers :
    (b : B) →
    is-retraction
      ( fiberwise-map-universal-property-family-of-fibers u G γ b)
      ( fiberwise-map-universal-property-family-of-fibers v F δ b)
  is-retraction-fiberwise-map-universal-property-family-of-fibers b =
    htpy-eq
      ( htpy-eq
        ( ap
          ( pr1)
          ( is-retraction-extension-universal-property-family-of-fibers))
        ( b))

  is-section-fiberwise-map-universal-property-family-of-fibers :
    (b : B) →
    is-section
      ( fiberwise-map-universal-property-family-of-fibers u G γ b)
      ( fiberwise-map-universal-property-family-of-fibers v F δ b)
  is-section-fiberwise-map-universal-property-family-of-fibers b =
    htpy-eq
      ( htpy-eq
        ( ap
          ( pr1)
          ( is-section-extension-universal-property-family-of-fibers))
        ( b))

  is-fiberwise-equiv-fiberwise-map-universal-property-family-of-fibers :
    is-fiberwise-equiv (fiberwise-map-universal-property-family-of-fibers u G γ)
  is-fiberwise-equiv-fiberwise-map-universal-property-family-of-fibers b =
    is-equiv-is-invertible
      ( family-of-elements-extension-double-lift-family-of-elements
        ( extension-universal-property-family-of-fibers v F δ)
        ( b))
      ( is-section-fiberwise-map-universal-property-family-of-fibers b)
      ( is-retraction-fiberwise-map-universal-property-family-of-fibers b)

  uniquely-unique-family-of-fibers :
    is-contr
      ( Σ ( fiberwise-equiv F G)
          ( λ h →
            ev-double-lift-family-of-elements δ (map-fiberwise-equiv h) ~ γ))
  uniquely-unique-family-of-fibers =
    is-torsorial-Eq-subtype
      ( uniqueness-extension-universal-property-family-of-fibers u G γ)
      ( is-property-is-fiberwise-equiv)
      ( fiberwise-map-universal-property-family-of-fibers u G γ)
      ( is-extension-fiberwise-map-universal-property-family-of-fibers u G γ)
      ( is-fiberwise-equiv-fiberwise-map-universal-property-family-of-fibers)

  extension-by-fiberwise-equiv-universal-property-family-of-fibers :
    Σ ( fiberwise-equiv F G)
      ( λ h → ev-double-lift-family-of-elements δ (map-fiberwise-equiv h) ~ γ)
  extension-by-fiberwise-equiv-universal-property-family-of-fibers =
    center uniquely-unique-family-of-fibers

  fiberwise-equiv-universal-property-of-fibers :
    fiberwise-equiv F G
  fiberwise-equiv-universal-property-of-fibers =
    pr1 extension-by-fiberwise-equiv-universal-property-family-of-fibers

  is-extension-fiberwise-equiv-universal-property-of-fibers :
    is-extension-double-lift-family-of-elements
      ( λ y _ → G y)
      ( δ)
      ( γ)
      ( map-fiberwise-equiv
        ( fiberwise-equiv-universal-property-of-fibers))
  is-extension-fiberwise-equiv-universal-property-of-fibers =
    pr2 extension-by-fiberwise-equiv-universal-property-family-of-fibers

A type family C over B satisfies the universal property of the family of fibers of a map f : A → B if and only if the constant map C b → (fiber f b → C b) is an equivalence for every b : B

In other words, the dependent type C is f-local if its fiber over b is fiber f b-null for every b : B.

This condition simplifies, for example, the proof that connected maps satisfy a dependent universal property.

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {f : A → B} {C : B → UU l3}
  where

  is-equiv-precomp-Π-fiber-condition :
    ((b : B) → is-equiv (diagonal-exponential (C b) (fiber f b))) →
    is-equiv (precomp-Π f C)
  is-equiv-precomp-Π-fiber-condition H =
    is-equiv-comp
      ( ev-lift-family-of-elements-fiber f (λ b _ → C b))
      ( map-Π (λ b → diagonal-exponential (C b) (fiber f b)))
      ( is-equiv-map-Π-is-fiberwise-equiv H)
      ( universal-property-family-of-fibers-fiber f C)

Computing the fibers of precomposition dependent functions as dependent products

We give four equivalences for the fibers of precomposition dependent functions as dependent products:

  fiber (precomp-Π f U) g
    ≃ (b : B) → Σ (u : U b), ((a , p) : fiber  f b) → g a ＝ₚᵁ u
    ≃ (b : B) → Σ (u : U b), ((a , p) : fiber' f b) → u ＝ₚᵁ g a
    ≃ (b : B) → Σ (u : U b), (a : A) (p : f a ＝ b) → g a ＝ₚᵁ u
    ≃ (b : B) → Σ (u : U b), (a : A) (p : b ＝ f a) → u ＝ₚᵁ g a

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

  family-dependent-product-fiber-precomp-Π : B → UU (l1 ⊔ l2 ⊔ l3)
  family-dependent-product-fiber-precomp-Π b =
    Σ (U b) (λ u → ((a , p) : fiber f b) → dependent-identification U p (g a) u)

  dependent-product-fiber-precomp-Π : UU (l1 ⊔ l2 ⊔ l3)
  dependent-product-fiber-precomp-Π =
    (b : B) → family-dependent-product-fiber-precomp-Π b

  dependent-product-characterization-fiber-precomp-Π :
    fiber (precomp-Π f U) g ≃ dependent-product-fiber-precomp-Π
  dependent-product-characterization-fiber-precomp-Π =
    equivalence-reasoning
      fiber (precomp-Π f U) g
      ≃ Σ ((b : B) → U b) (λ h → (a : A) → g a ＝ (h ∘ f) a)
        by compute-extension-fiber-precomp-Π f U g
      ≃ Σ ( (b : B) → U b)
          ( λ h → (b : B) ((a , p) : fiber f b) →
            dependent-identification U p (g a) (h b))
        by
          equiv-tot
            ( λ h →
              inv-equiv-dependent-universal-property-family-of-fibers f
                ( λ y (a , p) → dependent-identification U p (g a) (h y)))
      ≃ ( (b : B) →
          Σ ( U b)
            ( λ u →
              ((a , p) : fiber f b) → dependent-identification U p (g a) u))
        by inv-distributive-Π-Σ

  family-fiber-dependent-product-curry-precomp-Π : B → UU (l1 ⊔ l2 ⊔ l3)
  family-fiber-dependent-product-curry-precomp-Π b =
    Σ ( U b)
      ( λ u → (a : A) (p : f a ＝ b) → dependent-identification U p (g a) u)

  fiber-dependent-product-curry-precomp-Π : UU (l1 ⊔ l2 ⊔ l3)
  fiber-dependent-product-curry-precomp-Π =
    (b : B) → family-fiber-dependent-product-curry-precomp-Π b

  curried-dependent-product-characterization-fiber-precomp-Π :
    fiber (precomp-Π f U) g ≃ fiber-dependent-product-curry-precomp-Π
  curried-dependent-product-characterization-fiber-precomp-Π =
    ( equiv-Π-equiv-family (λ b → equiv-tot (λ u → equiv-ev-pair))) ∘e
    ( dependent-product-characterization-fiber-precomp-Π)

  family-dependent-product-fiber-precomp-Π' : B → UU (l1 ⊔ l2 ⊔ l3)
  family-dependent-product-fiber-precomp-Π' b =
    Σ ( U b)
      ( λ u → ((a , p) : fiber' f b) → dependent-identification U p u (g a))

  dependent-product-fiber-precomp-Π' : UU (l1 ⊔ l2 ⊔ l3)
  dependent-product-fiber-precomp-Π' =
    (b : B) → family-dependent-product-fiber-precomp-Π' b

  dependent-product-characterization-fiber-precomp-Π' :
    fiber (precomp-Π f U) g ≃ dependent-product-fiber-precomp-Π'
  dependent-product-characterization-fiber-precomp-Π' =
    equivalence-reasoning
      fiber (precomp-Π f U) g
      ≃ Σ ((b : B) → U b) (λ h → (a : A) → (h ∘ f) a ＝ g a)
        by compute-extension-fiber-precomp-Π' f U g
      ≃ Σ ( (b : B) → U b)
          ( λ h → (b : B) ((a , p) : fiber' f b) →
            dependent-identification U p (h b) (g a))
        by
          equiv-tot
            ( λ h →
              inv-equiv-dependent-universal-property-family-of-fibers' f
                ( λ y (a , p) → dependent-identification U p (h y) (g a)))
      ≃ ( (b : B) →
          Σ ( U b)
            ( λ u →
              ((a , p) : fiber' f b) → dependent-identification U p u (g a)))
        by inv-distributive-Π-Σ

  family-fiber-dependent-product-curry-precomp-Π' : B → UU (l1 ⊔ l2 ⊔ l3)
  family-fiber-dependent-product-curry-precomp-Π' b =
    Σ (U b) (λ u → (a : A) (p : b ＝ f a) → dependent-identification U p u (g a))

  fiber-dependent-product-curry-precomp-Π' : UU (l1 ⊔ l2 ⊔ l3)
  fiber-dependent-product-curry-precomp-Π' =
    (b : B) → family-fiber-dependent-product-curry-precomp-Π' b

  curried-dependent-product-characterization-fiber-precomp-Π' :
    fiber (precomp-Π f U) g ≃ fiber-dependent-product-curry-precomp-Π'
  curried-dependent-product-characterization-fiber-precomp-Π' =
    ( equiv-Π-equiv-family (λ b → equiv-tot (λ u → equiv-ev-pair))) ∘e
    ( dependent-product-characterization-fiber-precomp-Π')

Fibers of precomposition functions as dependent products

We give four equivalences for the fibers of precomposition functions as dependent products:

  fiber (precomp f U) g
    ≃ (b : B) → Σ (u : U), ((a , p) : fiber  f b) → g a ＝ u
    ≃ (b : B) → Σ (u : U), ((a , p) : fiber' f b) → u ＝ g a
    ≃ (b : B) → Σ (u : U), (a : A) → f a ＝ b → g a ＝ u
    ≃ (b : B) → Σ (u : U), (a : A) → b ＝ f a → u ＝ g a

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

  family-dependent-product-fiber-precomp : B → UU (l1 ⊔ l2 ⊔ l3)
  family-dependent-product-fiber-precomp b =
    Σ U (λ u → ((a , _) : fiber f b) → g a ＝ u)

  dependent-product-fiber-precomp : UU (l1 ⊔ l2 ⊔ l3)
  dependent-product-fiber-precomp =
    (b : B) → family-dependent-product-fiber-precomp b

  dependent-product-characterization-fiber-precomp :
    fiber (precomp f U) g ≃ dependent-product-fiber-precomp
  dependent-product-characterization-fiber-precomp =
    equivalence-reasoning
      fiber (precomp f U) g
      ≃ Σ (B → U) (λ h → (a : A) → g a ＝ (h ∘ f) a)
        by compute-extension-fiber-precomp f g
      ≃ Σ ( B → U)
          ( λ h → (b : B) ((a , _) : fiber f b) → g a ＝ h b)
        by
          equiv-tot
            ( λ h →
              inv-equiv-dependent-universal-property-family-of-fibers f
                ( λ y (a , _) → (g a ＝ h y)))
      ≃ ( (b : B) → Σ U (λ u → ((a , _) : fiber f b) → g a ＝ u))
        by inv-distributive-Π-Σ

  curried-dependent-product-characterization-fiber-precomp :
    fiber (precomp f U) g ≃ ((b : B) → Σ U (λ u → (a : A) → f a ＝ b → g a ＝ u))
  curried-dependent-product-characterization-fiber-precomp =
    ( equiv-Π-equiv-family (λ b → equiv-tot (λ u → equiv-ev-pair))) ∘e
    ( dependent-product-characterization-fiber-precomp)

  family-dependent-product-fiber-precomp' : B → UU (l1 ⊔ l2 ⊔ l3)
  family-dependent-product-fiber-precomp' b =
    Σ U (λ u → ((a , _) : fiber' f b) → u ＝ g a)

  dependent-product-fiber-precomp' : UU (l1 ⊔ l2 ⊔ l3)
  dependent-product-fiber-precomp' =
    (b : B) → family-dependent-product-fiber-precomp' b

  dependent-product-characterization-fiber-precomp' :
    fiber (precomp f U) g ≃ dependent-product-fiber-precomp'
  dependent-product-characterization-fiber-precomp' =
    equivalence-reasoning
      fiber (precomp f U) g
      ≃ Σ (B → U) (λ h → (h ∘ f) ~ g)
        by compute-extension-fiber-precomp' f g
      ≃ Σ ( B → U)
          ( λ h → (b : B) ((a , _) : fiber' f b) → h b ＝ g a)
        by
          equiv-tot
            ( λ h →
              inv-equiv-dependent-universal-property-family-of-fibers' f
                ( λ y (a , _) → (h y ＝ g a)))
      ≃ ( (b : B) → Σ U (λ u → ((a , _) : fiber' f b) → u ＝ g a))
        by inv-distributive-Π-Σ

  curried-dependent-product-characterization-fiber-precomp' :
    fiber (precomp f U) g ≃ ((b : B) → Σ U (λ u → (a : A) → b ＝ f a → u ＝ g a))
  curried-dependent-product-characterization-fiber-precomp' =
    ( equiv-Π-equiv-family (λ b → equiv-tot (λ u → equiv-ev-pair))) ∘e
    ( dependent-product-characterization-fiber-precomp')

Recent changes