Dependent products of pullbacks

Content created by Fredrik Bakke.

Created on 2024-03-02.
Last modified on 2024-03-02.

module foundation.dependent-products-pullbacks where
open import foundation.cones-over-cospan-diagrams
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.functoriality-dependent-function-types
open import foundation.identity-types
open import foundation.standard-pullbacks
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.pullbacks
open import foundation-core.retractions
open import foundation-core.sections
open import foundation-core.universal-property-pullbacks


Given a family of pullback squares

    Cᵢ -----> Bᵢ
    | ⌟       |
    |         | gᵢ
    ∨         ∨
    Aᵢ -----> Xᵢ

indexed by i : I, their dependent product

  Πᵢ Cᵢ -----> Πᵢ Bᵢ
    | ⌟          |
    |            | Πᵢ gᵢ
    ∨            ∨
  Πᵢ Aᵢ -----> Πᵢ Xᵢ
         Πᵢ fᵢ

is again a pullback square.


Dependent products of cones

module _
  {l1 l2 l3 l4 l5 : Level} {I : UU l1}
  {A : I  UU l2} {B : I  UU l3} {X : I  UU l4} {C : I  UU l5}
  (f : (i : I)  A i  X i) (g : (i : I)  B i  X i)
  (c : (i : I)  cone (f i) (g i) (C i))

  cone-Π : cone (map-Π f) (map-Π g) ((i : I)  C i)
  pr1 cone-Π = map-Π  i  pr1 (c i))
  pr1 (pr2 cone-Π) = map-Π  i  pr1 (pr2 (c i)))
  pr2 (pr2 cone-Π) = htpy-map-Π  i  pr2 (pr2 (c i)))


Computing the standard pullback of a dependent product

module _
  {l1 l2 l3 l4 : Level} {I : UU l1}
  {A : I  UU l2} {B : I  UU l3} {X : I  UU l4}
  (f : (i : I)  A i  X i) (g : (i : I)  B i  X i)

  map-standard-pullback-Π :
    standard-pullback (map-Π f) (map-Π g) 
    (i : I)  standard-pullback (f i) (g i)
  pr1 (map-standard-pullback-Π (α , β , γ) i) = α i
  pr1 (pr2 (map-standard-pullback-Π (α , β , γ) i)) = β i
  pr2 (pr2 (map-standard-pullback-Π (α , β , γ) i)) = htpy-eq γ i

  map-inv-standard-pullback-Π :
    ((i : I)  standard-pullback (f i) (g i)) 
    standard-pullback (map-Π f) (map-Π g)
  pr1 (map-inv-standard-pullback-Π h) i = pr1 (h i)
  pr1 (pr2 (map-inv-standard-pullback-Π h)) i = pr1 (pr2 (h i))
  pr2 (pr2 (map-inv-standard-pullback-Π h)) = eq-htpy  i  pr2 (pr2 (h i)))

    is-section-map-inv-standard-pullback-Π :
      is-section (map-standard-pullback-Π) (map-inv-standard-pullback-Π)
    is-section-map-inv-standard-pullback-Π h =
        ( λ i 
          map-extensionality-standard-pullback (f i) (g i) refl refl
            ( inv
              ( ( right-unit) 
                ( htpy-eq (is-section-eq-htpy  i  pr2 (pr2 (h i)))) i))))

    is-retraction-map-inv-standard-pullback-Π :
      is-retraction (map-standard-pullback-Π) (map-inv-standard-pullback-Π)
    is-retraction-map-inv-standard-pullback-Π (α , β , γ) =
        ( map-Π f)
        ( map-Π g)
        ( refl)
        ( refl)
        ( inv (right-unit  is-retraction-eq-htpy γ))

    is-equiv-map-standard-pullback-Π :
      is-equiv (map-standard-pullback-Π)
    is-equiv-map-standard-pullback-Π =
        ( map-inv-standard-pullback-Π)
        ( is-section-map-inv-standard-pullback-Π)
        ( is-retraction-map-inv-standard-pullback-Π)

  compute-standard-pullback-Π :
    ( standard-pullback (map-Π f) (map-Π g)) 
    ( (i : I)  standard-pullback (f i) (g i))
  compute-standard-pullback-Π =
    map-standard-pullback-Π , is-equiv-map-standard-pullback-Π

A dependent product of gap maps computes as the gap map of the dependent product

module _
  {l1 l2 l3 l4 l5 : Level} {I : UU l1}
  {A : I  UU l2} {B : I  UU l3} {X : I  UU l4} {C : I  UU l5}
  (f : (i : I)  A i  X i) (g : (i : I)  B i  X i)
  (c : (i : I)  cone (f i) (g i) (C i))

  triangle-map-standard-pullback-Π :
    map-Π  i  gap (f i) (g i) (c i)) ~
    map-standard-pullback-Π f g  gap (map-Π f) (map-Π g) (cone-Π f g c)
  triangle-map-standard-pullback-Π h =
      ( λ i 
          ( f i)
          ( g i)
          ( refl)
          ( refl)
          ( htpy-eq (is-section-eq-htpy _) i  inv right-unit))

Dependent products of pullbacks are pullbacks

module _
  {l1 l2 l3 l4 l5 : Level} {I : UU l1}
  {A : I  UU l2} {B : I  UU l3} {X : I  UU l4} {C : I  UU l5}
  (f : (i : I)  A i  X i) (g : (i : I)  B i  X i)
  (c : (i : I)  cone (f i) (g i) (C i))

    is-pullback-Π :
      ((i : I)  is-pullback (f i) (g i) (c i)) 
      is-pullback (map-Π f) (map-Π g) (cone-Π f g c)
    is-pullback-Π is-pb-c =
        ( map-Π  i  gap (f i) (g i) (c i)))
        ( map-standard-pullback-Π f g)
        ( gap (map-Π f) (map-Π g) (cone-Π f g c))
        ( triangle-map-standard-pullback-Π f g c)
        ( is-equiv-map-standard-pullback-Π f g)
        ( is-equiv-map-Π-is-fiberwise-equiv is-pb-c)

Cones satisfying the universal property of pullbacks are closed under dependent products

module _
  {l1 l2 l3 l4 l5 : Level} {I : UU l1}
  {A : I  UU l2} {B : I  UU l3} {X : I  UU l4}
  (f : (i : I)  A i  X i) (g : (i : I)  B i  X i)
  {C : I  UU l5} (c : (i : I)  cone (f i) (g i) (C i))

  universal-property-pullback-Π :
    ((i : I)  universal-property-pullback (f i) (g i) (c i)) 
    universal-property-pullback (map-Π f) (map-Π g) (cone-Π f g c)
  universal-property-pullback-Π H =
      ( map-Π f)
      ( map-Π g)
      ( cone-Π f g c)
      ( is-pullback-Π f g c
        ( λ i 
          is-pullback-universal-property-pullback (f i) (g i) (c i) (H i)))

Table of files about pullbacks

The following table lists files that are about pullbacks as a general concept.

Cospan diagramsfoundation.cospans
Morphisms of cospan diagramsfoundation.morphisms-cospans
Cones over cospan diagramsfoundation.cones-over-cospan-diagrams
The universal property of pullbacks (foundation-core)foundation-core.universal-property-pullbacks
The universal property of pullbacks (foundation)foundation.universal-property-pullbacks
The universal property of fiber productsfoundation.universal-property-fiber-products
Standard pullbacksfoundation.standard-pullbacks
Pullbacks (foundation-core)foundation-core.pullbacks
Pullbacks (foundation)foundation.pullbacks
Functoriality of pullbacksfoundation.functoriality-pullbacks
Cartesian morphisms of arrowsfoundation.cartesian-morphisms-arrows
Dependent products of pullbacksfoundation.dependent-products-pullbacks
Dependent sums of pullbacksfoundation.dependent-sums-pullbacks
Products of pullbacksfoundation.products-pullbacks
Coroducts of pullbacksfoundation.coproducts-pullbacks
Postcomposition of pullbacksfoundation.postcomposition-pullbacks
Pullbacks of subtypesfoundation.pullbacks-subtypes
The pullback-homorthogonal-factorization-systems.pullback-hom
Functoriality of the pullback-homorthogonal-factorization-systems.functoriality-pullback-hom
Pullbacks in precategoriescategory-theory.pullbacks-in-precategories

Recent changes