# Dependent sums of pullbacks

Content created by Fredrik Bakke.

Created on 2024-03-02.

module foundation.dependent-sums-pullbacks where

Imports
open import foundation.cones-over-cospan-diagrams
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.standard-pullbacks
open import foundation.transport-along-identifications
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import foundation-core.equality-dependent-pair-types
open import foundation-core.families-of-equivalences
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-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


## Properties

### Computing the standard pullback of a dependent sum

Squares of the form

  Σ (x : A) (Q (f x)) ----> Σ (y : B) Q
|                          |
|                          |
pr1 |                          | pr1
|                          |
∨                          ∨
A -----------------------> B
f


are pullbacks.

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

standard-pullback-Σ : UU (l1 ⊔ l3)
standard-pullback-Σ = Σ A (λ x → Q (f x))

cone-standard-pullback-Σ : cone f pr1 standard-pullback-Σ
pr1 cone-standard-pullback-Σ = pr1
pr1 (pr2 cone-standard-pullback-Σ) = map-Σ-map-base f Q
pr2 (pr2 cone-standard-pullback-Σ) = refl-htpy

inv-gap-cone-standard-pullback-Σ :
standard-pullback f (pr1 {B = Q}) → standard-pullback-Σ
pr1 (inv-gap-cone-standard-pullback-Σ (x , _)) = x
pr2 (inv-gap-cone-standard-pullback-Σ (x , (.(f x) , q) , refl)) = q

abstract
is-section-inv-gap-cone-standard-pullback-Σ :
is-section
( gap f pr1 cone-standard-pullback-Σ)
( inv-gap-cone-standard-pullback-Σ)
is-section-inv-gap-cone-standard-pullback-Σ (x , (.(f x) , q) , refl) = refl

abstract
is-retraction-inv-gap-cone-standard-pullback-Σ :
is-retraction
( gap f pr1 cone-standard-pullback-Σ)
( inv-gap-cone-standard-pullback-Σ)
is-retraction-inv-gap-cone-standard-pullback-Σ = refl-htpy

abstract
is-pullback-cone-standard-pullback-Σ :
is-pullback f pr1 cone-standard-pullback-Σ
is-pullback-cone-standard-pullback-Σ =
is-equiv-is-invertible
inv-gap-cone-standard-pullback-Σ
is-section-inv-gap-cone-standard-pullback-Σ
is-retraction-inv-gap-cone-standard-pullback-Σ

compute-standard-pullback-Σ :
standard-pullback-Σ ≃ standard-pullback f pr1
pr1 compute-standard-pullback-Σ = gap f pr1 cone-standard-pullback-Σ
pr2 compute-standard-pullback-Σ = is-pullback-cone-standard-pullback-Σ


### A family of maps over a base map induces a pullback square if and only if it is a family of equivalences

Given a map f : A → B with a family of maps over it g : (x : A) → P x → Q (f x), then the square

         map-Σ f g
Σ A P ----------> Σ B Q
|                |
|                |
∨                ∨
A -------------> B
f


is a pullback if and only if g is a fiberwise equivalence.

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {P : A → UU l3}
(Q : B → UU l4) (f : A → B) (g : (x : A) → P x → Q (f x))
where

cone-map-Σ : cone f pr1 (Σ A P)
pr1 cone-map-Σ = pr1
pr1 (pr2 cone-map-Σ) = map-Σ Q f g
pr2 (pr2 cone-map-Σ) = refl-htpy

abstract
is-pullback-is-fiberwise-equiv :
is-fiberwise-equiv g → is-pullback f pr1 cone-map-Σ
is-pullback-is-fiberwise-equiv is-equiv-g =
is-equiv-comp
( gap f pr1 (cone-standard-pullback-Σ f Q))
( tot g)
( is-equiv-tot-is-fiberwise-equiv is-equiv-g)
( is-pullback-cone-standard-pullback-Σ f Q)

abstract
universal-property-pullback-is-fiberwise-equiv :
is-fiberwise-equiv g →
universal-property-pullback f pr1 cone-map-Σ
universal-property-pullback-is-fiberwise-equiv is-equiv-g =
universal-property-pullback-is-pullback f pr1
( cone-map-Σ)
( is-pullback-is-fiberwise-equiv is-equiv-g)

abstract
is-fiberwise-equiv-is-pullback :
is-pullback f pr1 cone-map-Σ → is-fiberwise-equiv g
is-fiberwise-equiv-is-pullback is-pullback-cone-map-Σ =
is-fiberwise-equiv-is-equiv-tot
( is-equiv-right-factor
( gap f pr1 (cone-standard-pullback-Σ f Q))
( tot g)
( is-pullback-cone-standard-pullback-Σ f Q)
( is-pullback-cone-map-Σ))

abstract
is-fiberwise-equiv-universal-property-pullback :
( universal-property-pullback f pr1 cone-map-Σ) →
is-fiberwise-equiv g
is-fiberwise-equiv-universal-property-pullback up =
is-fiberwise-equiv-is-pullback
( is-pullback-universal-property-pullback f pr1 cone-map-Σ up)


### Pullbacks are preserved by dependent sums

#### A family of squares over a pullback square is a family of pullback squares if and only if the total square is a pullback

module _
{l1 l2 l3 l4 l5 l6 l7 l8 : Level}
{X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
(PX : X → UU l5) {PA : A → UU l6} {PB : B → UU l7} {PC : C → UU l8}
{f : A → X} {g : B → X}
(f' : (a : A) → PA a → PX (f a)) (g' : (b : B) → PB b → PX (g b))
(c : cone f g C) (c' : cone-family PX f' g' c PC)
where

tot-cone-cone-family :
cone (map-Σ PX f f') (map-Σ PX g g') (Σ C PC)
pr1 tot-cone-cone-family =
map-Σ _ (vertical-map-cone f g c) (λ x → pr1 (c' x))
pr1 (pr2 tot-cone-cone-family) =
map-Σ _ (horizontal-map-cone f g c) (λ x → (pr1 (pr2 (c' x))))
pr2 (pr2 tot-cone-cone-family) =
htpy-map-Σ PX
( coherence-square-cone f g c)
( λ z →
( f' (vertical-map-cone f g c z)) ∘
( vertical-map-cone
( ( tr PX (coherence-square-cone f g c z)) ∘
( f' (vertical-map-cone f g c z)))
( g' (horizontal-map-cone f g c z))
( c' z)))
( λ z →
coherence-square-cone
( ( tr PX (coherence-square-cone f g c z)) ∘
( f' (vertical-map-cone f g c z)))
( g' (horizontal-map-cone f g c z))
( c' z))

map-standard-pullback-tot-cone-cone-fam-right-factor :
Σ ( standard-pullback f g)
( λ t →
standard-pullback
( tr PX (coherence-square-standard-pullback t) ∘
f' (vertical-map-standard-pullback t))
( g' (horizontal-map-standard-pullback t))) →
Σ ( Σ A PA)
( λ aa' → Σ (Σ B (λ b → f (pr1 aa') ＝ g b))
( λ bα → Σ (PB (pr1 bα))
( λ b' → tr PX (pr2 bα) (f' (pr1 aa') (pr2 aa')) ＝ g' (pr1 bα) b')))
map-standard-pullback-tot-cone-cone-fam-right-factor =
map-interchange-Σ-Σ
( λ a bα a' →
Σ ( PB (pr1 bα))
( λ b' → tr PX (pr2 bα) (f' a a') ＝ g' (pr1 bα) b'))

map-standard-pullback-tot-cone-cone-fam-left-factor :
(aa' : Σ A PA) →
Σ (Σ B (λ b → f (pr1 aa') ＝ g b))
( λ bα →
Σ ( PB (pr1 bα))
( λ b' → tr PX (pr2 bα) (f' (pr1 aa') (pr2 aa')) ＝ g' (pr1 bα) b')) →
Σ ( Σ B PB)
( λ bb' → Σ (f (pr1 aa') ＝ g (pr1 bb'))
( λ α → tr PX α (f' (pr1 aa') (pr2 aa')) ＝ g' (pr1 bb') (pr2 bb')))
map-standard-pullback-tot-cone-cone-fam-left-factor aa' =
( map-interchange-Σ-Σ
( λ b α b' → tr PX α (f' (pr1 aa') (pr2 aa')) ＝ g' b b'))

map-standard-pullback-tot-cone-cone-family :
Σ ( standard-pullback f g)
( λ t →
standard-pullback
( ( tr PX (coherence-square-standard-pullback t)) ∘
( f' (vertical-map-standard-pullback t)))
( g' (horizontal-map-standard-pullback t))) →
standard-pullback (map-Σ PX f f') (map-Σ PX g g')
map-standard-pullback-tot-cone-cone-family =
( tot
(λ aa' →
( tot (λ bb' → eq-pair-Σ')) ∘
( map-standard-pullback-tot-cone-cone-fam-left-factor aa'))) ∘
( map-standard-pullback-tot-cone-cone-fam-right-factor)

is-equiv-map-standard-pullback-tot-cone-cone-family :
is-equiv map-standard-pullback-tot-cone-cone-family
is-equiv-map-standard-pullback-tot-cone-cone-family =
is-equiv-comp
( tot
( λ aa' →
( tot (λ bb' → eq-pair-Σ')) ∘
( map-standard-pullback-tot-cone-cone-fam-left-factor aa')))
( map-standard-pullback-tot-cone-cone-fam-right-factor)
( is-equiv-map-interchange-Σ-Σ
( λ a bα a' → Σ (PB (pr1 bα))
( λ b' → tr PX (pr2 bα) (f' a a') ＝ g' (pr1 bα) b')))
( is-equiv-tot-is-fiberwise-equiv
( λ aa' →
is-equiv-comp
( tot (λ bb' → eq-pair-Σ'))
( map-standard-pullback-tot-cone-cone-fam-left-factor aa')
( is-equiv-map-interchange-Σ-Σ _)
( is-equiv-tot-is-fiberwise-equiv
( λ bb' →
is-equiv-eq-pair-Σ
( f (pr1 aa') , f' (pr1 aa') (pr2 aa'))
( g (pr1 bb') , g' (pr1 bb') (pr2 bb'))))))

triangle-standard-pullback-tot-cone-cone-family :
( gap (map-Σ PX f f') (map-Σ PX g g') tot-cone-cone-family) ~
( ( map-standard-pullback-tot-cone-cone-family) ∘
( map-Σ _
( gap f g c)
( λ x → gap
( ( tr PX (coherence-square-cone f g c x)) ∘
( f' (vertical-map-cone f g c x)))
( g' (horizontal-map-cone f g c x))
( c' x))))
triangle-standard-pullback-tot-cone-cone-family = refl-htpy

is-pullback-family-is-pullback-tot :
is-pullback f g c →
is-pullback
(map-Σ PX f f') (map-Σ PX g g') tot-cone-cone-family →
(x : C) →
is-pullback
( ( tr PX (coherence-square-cone f g c x)) ∘
( f' (vertical-map-cone f g c x)))
( g' (horizontal-map-cone f g c x))
( c' x)
is-pullback-family-is-pullback-tot is-pb-c is-pb-tot =
is-fiberwise-equiv-is-equiv-map-Σ _
( gap f g c)
( λ x →
gap
( ( tr PX (coherence-square-cone f g c x)) ∘
( f' (vertical-map-cone f g c x)))
( g' (horizontal-map-cone f g c x))
( c' x))
( is-pb-c)
( is-equiv-top-map-triangle
( gap (map-Σ PX f f') (map-Σ PX g g') tot-cone-cone-family)
( map-standard-pullback-tot-cone-cone-family)
( map-Σ _
( gap f g c)
( λ x →
gap
( ( tr PX (coherence-square-cone f g c x)) ∘
( f' (vertical-map-cone f g c x)))
( g' (horizontal-map-cone f g c x))
( c' x)))
( triangle-standard-pullback-tot-cone-cone-family)
( is-equiv-map-standard-pullback-tot-cone-cone-family)
( is-pb-tot))

is-pullback-tot-is-pullback-family :
is-pullback f g c →
( (x : C) →
is-pullback
( ( tr PX (coherence-square-cone f g c x)) ∘
( f' (vertical-map-cone f g c x)))
( g' (horizontal-map-cone f g c x))
( c' x)) →
is-pullback
(map-Σ PX f f') (map-Σ PX g g') tot-cone-cone-family
is-pullback-tot-is-pullback-family is-pb-c is-pb-c' =
is-equiv-left-map-triangle
( gap (map-Σ PX f f') (map-Σ PX g g') tot-cone-cone-family)
( map-standard-pullback-tot-cone-cone-family)
( map-Σ _
( gap f g c)
( λ x → gap
( ( tr PX (coherence-square-cone f g c x)) ∘
( f' (vertical-map-cone f g c x)))
( g' (horizontal-map-cone f g c x))
( c' x)))
( triangle-standard-pullback-tot-cone-cone-family)
( is-equiv-map-Σ _ is-pb-c is-pb-c')
( is-equiv-map-standard-pullback-tot-cone-cone-family)


#### A family of squares is a family of pullback squares if and only if the total square is a pullback

As a corollary of the previous result, a dependent sum of squares over the constant diagram is a pullback square if and only if the family is a family of pullback squares.

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

tot-cone : cone (tot f) (tot g) (Σ I A)
pr1 tot-cone = tot (λ i → vertical-map-cone (f i) (g i) (c i))
pr1 (pr2 tot-cone) = tot (λ i → horizontal-map-cone (f i) (g i) (c i))
pr2 (pr2 tot-cone) = tot-htpy (λ i → coherence-square-cone (f i) (g i) (c i))

is-pullback-tot-is-pullback-family-id-cone :
((i : I) → is-pullback (f i) (g i) (c i)) →
is-pullback (tot f) (tot g) tot-cone
is-pullback-tot-is-pullback-family-id-cone =
is-pullback-tot-is-pullback-family Y f g
( id-cone I)
( c)
( is-pullback-is-equiv-vertical-maps id id
( id-cone I)
( is-equiv-id)
( is-equiv-id))

is-pullback-family-id-cone-is-pullback-tot :
is-pullback (tot f) (tot g) tot-cone →
(i : I) → is-pullback (f i) (g i) (c i)
is-pullback-family-id-cone-is-pullback-tot =
is-pullback-family-is-pullback-tot Y f g
( id-cone I)
( c)
( is-pullback-is-equiv-vertical-maps id id
( id-cone I)
( is-equiv-id)
( is-equiv-id))


## Table of files about pullbacks

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

ConceptFile
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