# Standard pullbacks

Content created by Fredrik Bakke.

Created on 2024-03-02.

module foundation.standard-pullbacks where

Imports
open import foundation.action-on-identifications-functions
open import foundation.cones-over-cospan-diagrams
open import foundation.dependent-pair-types
open import foundation.equality-cartesian-product-types
open import foundation.functoriality-cartesian-product-types
open import foundation.identity-types
open import foundation.structure-identity-principle
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.commuting-squares-of-maps
open import foundation-core.diagonal-maps-cartesian-products-of-types
open import foundation-core.equality-dependent-pair-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.retractions
open import foundation-core.sections
open import foundation-core.type-theoretic-principle-of-choice
open import foundation-core.universal-property-pullbacks
open import foundation-core.whiskering-identifications-concatenation


## Idea

Given a cospan of types

  f : A → X ← B : g,


we can form the standard pullback A ×_X B satisfying the universal property of the pullback of the cospan, completing the diagram

  A ×_X B ------> B
| ⌟          |
|            | g
|            |
∨            ∨
A ---------> X.
f


The standard pullback consists of pairs a : A and b : B such that f a and g b agree:

  A ×_X B := Σ (a : A) (b : B), (f a ＝ g b),


thus the standard cone consists of the canonical projections.

## Definitions

### The standard pullback of a cospan

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

standard-pullback : UU (l1 ⊔ l2 ⊔ l3)
standard-pullback = Σ A (λ x → Σ B (λ y → f x ＝ g y))

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

vertical-map-standard-pullback : standard-pullback f g → A
vertical-map-standard-pullback = pr1

horizontal-map-standard-pullback : standard-pullback f g → B
horizontal-map-standard-pullback t = pr1 (pr2 t)

coherence-square-standard-pullback :
coherence-square-maps
( horizontal-map-standard-pullback)
( vertical-map-standard-pullback)
( g)
( f)
coherence-square-standard-pullback t = pr2 (pr2 t)


### The cone at the standard pullback

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

cone-standard-pullback : cone f g (standard-pullback f g)
pr1 cone-standard-pullback = vertical-map-standard-pullback
pr1 (pr2 cone-standard-pullback) = horizontal-map-standard-pullback
pr2 (pr2 cone-standard-pullback) = coherence-square-standard-pullback


### The gap map into the standard pullback

The standard gap map of a commuting square is the map from the domain of the cone into the standard pullback.

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

gap : cone f g C → C → standard-pullback f g
pr1 (gap c z) = vertical-map-cone f g c z
pr1 (pr2 (gap c z)) = horizontal-map-cone f g c z
pr2 (pr2 (gap c z)) = coherence-square-cone f g c z


#### The standard ternary pullback

Given two cospans with a shared vertex B:

      f       g       h       i
A ----> X <---- B ----> Y <---- C,


we call the standard limit of the diagram the standard ternary pullback. It is defined as the sum

  standard-ternary-pullback f g h i :=
Σ (a : A) (b : B) (c : C), ((f a ＝ g b) × (h b ＝ i c)).

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

standard-ternary-pullback : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
standard-ternary-pullback =
Σ A (λ a → Σ B (λ b → Σ C (λ c → (f a ＝ g b) × (h b ＝ i c))))


## Properties

### Characterization of the identity type of the standard pullback

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

Eq-standard-pullback : (t t' : standard-pullback f g) → UU (l1 ⊔ l2 ⊔ l3)
Eq-standard-pullback (a , b , p) (a' , b' , p') =
Σ (a ＝ a') (λ α → Σ (b ＝ b') (λ β → ap f α ∙ p' ＝ p ∙ ap g β))

refl-Eq-standard-pullback :
(t : standard-pullback f g) → Eq-standard-pullback t t
pr1 (refl-Eq-standard-pullback (a , b , p)) = refl
pr1 (pr2 (refl-Eq-standard-pullback (a , b , p))) = refl
pr2 (pr2 (refl-Eq-standard-pullback (a , b , p))) = inv right-unit

Eq-eq-standard-pullback :
(s t : standard-pullback f g) → s ＝ t → Eq-standard-pullback s t
Eq-eq-standard-pullback s .s refl = refl-Eq-standard-pullback s

extensionality-standard-pullback :
(t t' : standard-pullback f g) → (t ＝ t') ≃ Eq-standard-pullback t t'
extensionality-standard-pullback (a , b , p) =
extensionality-Σ
( λ bp' α → Σ (b ＝ pr1 bp') (λ β → ap f α ∙ pr2 bp' ＝ p ∙ ap g β))
( refl)
( refl , inv right-unit)
( λ x → id-equiv)
( extensionality-Σ
( λ p' β → p' ＝ p ∙ ap g β)
( refl)
( inv right-unit)
( λ y → id-equiv)
( λ p' → equiv-concat' p' (inv right-unit) ∘e equiv-inv p p'))

map-extensionality-standard-pullback :
{ s t : standard-pullback f g}
( α : vertical-map-standard-pullback s ＝ vertical-map-standard-pullback t)
( β :
horizontal-map-standard-pullback s ＝
horizontal-map-standard-pullback t) →
( ( ap f α ∙ coherence-square-standard-pullback t) ＝
( coherence-square-standard-pullback s ∙ ap g β)) →
s ＝ t
map-extensionality-standard-pullback {s} {t} α β γ =
map-inv-equiv (extensionality-standard-pullback s t) (α , β , γ)


### The standard pullback satisfies the universal property of pullbacks

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

abstract
universal-property-standard-pullback :
universal-property-pullback f g (cone-standard-pullback f g)
universal-property-standard-pullback C =
is-equiv-comp
( tot (λ _ → map-distributive-Π-Σ))
( mapping-into-Σ)
( is-equiv-mapping-into-Σ)
( is-equiv-tot-is-fiberwise-equiv (λ _ → is-equiv-map-distributive-Π-Σ))


### A cone is equal to the value of cone-map at its own gap map

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

htpy-cone-up-pullback-standard-pullback :
(c : cone f g C) →
htpy-cone f g (cone-map f g (cone-standard-pullback f g) (gap f g c)) c
pr1 (htpy-cone-up-pullback-standard-pullback c) = refl-htpy
pr1 (pr2 (htpy-cone-up-pullback-standard-pullback c)) = refl-htpy
pr2 (pr2 (htpy-cone-up-pullback-standard-pullback c)) = right-unit-htpy


### Standard pullbacks are symmetric

The standard pullback of f : A -> X <- B : g is equivalent to the standard pullback of g : B -> X <- A : f.

map-commutative-standard-pullback :
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
(f : A → X) (g : B → X) → standard-pullback f g → standard-pullback g f
pr1 (map-commutative-standard-pullback f g x) =
horizontal-map-standard-pullback x
pr1 (pr2 (map-commutative-standard-pullback f g x)) =
vertical-map-standard-pullback x
pr2 (pr2 (map-commutative-standard-pullback f g x)) =
inv (coherence-square-standard-pullback x)

inv-inv-map-commutative-standard-pullback :
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
(f : A → X) (g : B → X) →
( map-commutative-standard-pullback f g ∘
map-commutative-standard-pullback g f) ~ id
inv-inv-map-commutative-standard-pullback f g x =
eq-pair-eq-fiber
( eq-pair-eq-fiber
( inv-inv (coherence-square-standard-pullback x)))

abstract
is-equiv-map-commutative-standard-pullback :
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
(f : A → X) (g : B → X) → is-equiv (map-commutative-standard-pullback f g)
is-equiv-map-commutative-standard-pullback f g =
is-equiv-is-invertible
( map-commutative-standard-pullback g f)
( inv-inv-map-commutative-standard-pullback f g)
( inv-inv-map-commutative-standard-pullback g f)

commutative-standard-pullback :
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
(f : A → X) (g : B → X) →
standard-pullback f g ≃ standard-pullback g f
pr1 (commutative-standard-pullback f g) =
map-commutative-standard-pullback f g
pr2 (commutative-standard-pullback f g) =
is-equiv-map-commutative-standard-pullback f g


#### The gap map of the swapped cone computes as the underlying gap map followed by a swap

triangle-map-commutative-standard-pullback :
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
(f : A → X) (g : B → X) (c : cone f g C) →
gap g f (swap-cone f g c) ~
map-commutative-standard-pullback f g ∘ gap f g c
triangle-map-commutative-standard-pullback f g c = refl-htpy


### Standard pullbacks are associative

Consider two cospans with a shared vertex B:

      f       g       h       i
A ----> X <---- B ----> Y <---- C,


then we can construct their limit using standard pullbacks in two equivalent ways. We can construct it by first forming the standard pullback of f and g, and then forming the standard pullback of the resulting h ∘ f' and i

  (A ×_X B) ×_Y C ---------------------> C
| ⌟                             |
|                               | i
∨                               ∨
A ×_X B ---------> B ------------> Y
| ⌟     f'      |       h
|               | g
∨               ∨
A ------------> X,
f


or we can first form the pullback of h and i, and then form the pullback of f and the resulting g ∘ i':

  A ×_X (B ×_Y C) --> B ×_Y C ---------> C
| ⌟             | ⌟             |
|               | i'            | i
|               ∨               ∨
|               B ------------> Y
|               |       h
|               | g
∨               ∨
A ------------> X.
f


We show that both of these constructions are equivalent by showing they are equivalent to the standard ternary pullback.

Note: Associativity with respect to ternary cospans

              B
|
| g
∨
A ------> X <------ C
f         h


is a special case of what we consider here that is recovered by using

      f       g       g       h
A ----> X <---- B ----> X <---- C.


#### Computing the left associated iterated standard pullback

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

map-left-associative-standard-pullback :
standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i →
standard-ternary-pullback f g h i
map-left-associative-standard-pullback ((a , b , p) , c , q) =
( a , b , c , p , q)

map-inv-left-associative-standard-pullback :
standard-ternary-pullback f g h i →
standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i
map-inv-left-associative-standard-pullback (a , b , c , p , q) =
( ( a , b , p) , c , q)

is-equiv-map-left-associative-standard-pullback :
is-equiv map-left-associative-standard-pullback
is-equiv-map-left-associative-standard-pullback =
is-equiv-is-invertible
( map-inv-left-associative-standard-pullback)
( refl-htpy)
( refl-htpy)

compute-left-associative-standard-pullback :
standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i ≃
standard-ternary-pullback f g h i
compute-left-associative-standard-pullback =
( map-left-associative-standard-pullback ,
is-equiv-map-left-associative-standard-pullback)


#### Computing the right associated iterated dependent pullback

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

map-right-associative-standard-pullback :
standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) →
standard-ternary-pullback f g h i
map-right-associative-standard-pullback (a , (b , c , p) , q) =
( a , b , c , q , p)

map-inv-right-associative-standard-pullback :
standard-ternary-pullback f g h i →
standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i})
map-inv-right-associative-standard-pullback (a , b , c , p , q) =
( a , (b , c , q) , p)

is-equiv-map-right-associative-standard-pullback :
is-equiv map-right-associative-standard-pullback
is-equiv-map-right-associative-standard-pullback =
is-equiv-is-invertible
( map-inv-right-associative-standard-pullback)
( refl-htpy)
( refl-htpy)

compute-right-associative-standard-pullback :
standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) ≃
standard-ternary-pullback f g h i
compute-right-associative-standard-pullback =
( map-right-associative-standard-pullback ,
is-equiv-map-right-associative-standard-pullback)


#### Standard pullbacks are associative

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

associative-standard-pullback :
standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i ≃
standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i})
associative-standard-pullback =
( inv-equiv (compute-right-associative-standard-pullback f g h i)) ∘e
( compute-left-associative-standard-pullback f g h i)

map-associative-standard-pullback :
standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i →
standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i})
map-associative-standard-pullback = map-equiv associative-standard-pullback

map-inv-associative-standard-pullback :
standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) →
standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i
map-inv-associative-standard-pullback =
map-inv-equiv associative-standard-pullback


### Pullbacks can be "folded"

Given a standard pullback square

         f'
C -------> B
| ⌟        |
g'|          | g
∨          ∨
A -------> X
f


we can "fold" the vertical edge onto the horizontal one and get a new pullback square

            C ---------> X
| ⌟          |
(f' , g') |            |
∨            ∨
A × B -----> X × X,
f × g


moreover, this folded square is a pullback if and only if the original one is.

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

fold-cone :
{l4 : Level} {C : UU l4} →
cone f g C → cone (map-product f g) (diagonal-product X) C
pr1 (pr1 (fold-cone c) z) = vertical-map-cone f g c z
pr2 (pr1 (fold-cone c) z) = horizontal-map-cone f g c z
pr1 (pr2 (fold-cone c)) = g ∘ horizontal-map-cone f g c
pr2 (pr2 (fold-cone c)) z = eq-pair (coherence-square-cone f g c z) refl

map-fold-cone-standard-pullback :
standard-pullback f g →
standard-pullback (map-product f g) (diagonal-product X)
pr1 (pr1 (map-fold-cone-standard-pullback x)) =
vertical-map-standard-pullback x
pr2 (pr1 (map-fold-cone-standard-pullback x)) =
horizontal-map-standard-pullback x
pr1 (pr2 (map-fold-cone-standard-pullback x)) =
g (horizontal-map-standard-pullback x)
pr2 (pr2 (map-fold-cone-standard-pullback x)) =
eq-pair (coherence-square-standard-pullback x) refl

map-inv-fold-cone-standard-pullback :
standard-pullback (map-product f g) (diagonal-product X) →
standard-pullback f g
pr1 (map-inv-fold-cone-standard-pullback ((a , b) , x , α)) = a
pr1 (pr2 (map-inv-fold-cone-standard-pullback ((a , b) , x , α))) = b
pr2 (pr2 (map-inv-fold-cone-standard-pullback ((a , b) , x , α))) =
ap pr1 α ∙ inv (ap pr2 α)

abstract
is-section-map-inv-fold-cone-standard-pullback :
is-section
( map-fold-cone-standard-pullback)
( map-inv-fold-cone-standard-pullback)
is-section-map-inv-fold-cone-standard-pullback ((a , b) , (x , α)) =
map-extensionality-standard-pullback
( map-product f g)
( diagonal-product X)
( refl)
( ap pr2 α)
( ( inv (is-section-pair-eq α)) ∙
( ap
( λ t → eq-pair t (ap pr2 α))
( ( inv right-unit) ∙
( inv
( left-whisker-concat
( ap pr1 α)
( left-inv (ap pr2 α)))) ∙
( inv (assoc (ap pr1 α) (inv (ap pr2 α)) (ap pr2 α))))) ∙
( eq-pair-concat
( ap pr1 α ∙ inv (ap pr2 α))
( ap pr2 α)
( refl)
( ap pr2 α)) ∙
( ap
( concat (eq-pair (ap pr1 α ∙ inv (ap pr2 α)) refl) (x , x))
( inv (compute-ap-diagonal-product (ap pr2 α)))))

abstract
is-retraction-map-inv-fold-cone-standard-pullback :
is-retraction
( map-fold-cone-standard-pullback)
( map-inv-fold-cone-standard-pullback)
is-retraction-map-inv-fold-cone-standard-pullback (a , b , p) =
map-extensionality-standard-pullback f g
( refl)
( refl)
( inv
( ( right-whisker-concat
( ( right-whisker-concat
( ap-pr1-eq-pair p refl)
( inv (ap pr2 (eq-pair p refl)))) ∙
( ap (λ t → p ∙ inv t) (ap-pr2-eq-pair p refl)) ∙
( right-unit))
( refl)) ∙
( right-unit)))

abstract
is-equiv-map-fold-cone-standard-pullback :
is-equiv map-fold-cone-standard-pullback
is-equiv-map-fold-cone-standard-pullback =
is-equiv-is-invertible
( map-inv-fold-cone-standard-pullback)
( is-section-map-inv-fold-cone-standard-pullback)
( is-retraction-map-inv-fold-cone-standard-pullback)

compute-fold-standard-pullback :
standard-pullback f g ≃
standard-pullback (map-product f g) (diagonal-product X)
compute-fold-standard-pullback =
map-fold-cone-standard-pullback , is-equiv-map-fold-cone-standard-pullback

triangle-map-fold-cone-standard-pullback :
{l4 : Level} {C : UU l4} (c : cone f g C) →
gap (map-product f g) (diagonal-product X) (fold-cone c) ~
map-fold-cone-standard-pullback ∘ gap f g c
triangle-map-fold-cone-standard-pullback c = refl-htpy


### The equivalence on standard pullbacks induced by parallel cospans

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
{f f' : A → X} (Hf : f ~ f') {g g' : B → X} (Hg : g ~ g')
where

map-equiv-standard-pullback-htpy :
standard-pullback f' g' → standard-pullback f g
map-equiv-standard-pullback-htpy =
tot (λ a → tot (λ b → concat' (f a) (inv (Hg b)) ∘ concat (Hf a) (g' b)))

abstract
is-equiv-map-equiv-standard-pullback-htpy :
is-equiv map-equiv-standard-pullback-htpy
is-equiv-map-equiv-standard-pullback-htpy =
is-equiv-tot-is-fiberwise-equiv
( λ a →
is-equiv-tot-is-fiberwise-equiv
( λ b →
is-equiv-comp
( concat' (f a) (inv (Hg b)))
( concat (Hf a) (g' b))
( is-equiv-concat (Hf a) (g' b))
( is-equiv-concat' (f a) (inv (Hg b)))))

equiv-standard-pullback-htpy :
standard-pullback f' g' ≃ standard-pullback f g
pr1 equiv-standard-pullback-htpy = map-equiv-standard-pullback-htpy
pr2 equiv-standard-pullback-htpy = is-equiv-map-equiv-standard-pullback-htpy


## 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