# Postcomposition of pullbacks

Content created by Fredrik Bakke.

Created on 2024-03-02.

module foundation.postcomposition-pullbacks where

Imports
open import foundation.cones-over-cospan-diagrams
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.identity-types
open import foundation.standard-pullbacks
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.commuting-triangles-of-maps
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.postcomposition-functions
open import foundation-core.pullbacks
open import foundation-core.universal-property-pullbacks


## Idea

Given a pullback square

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


then the exponentiated square given by postcomposition

                f' ∘ -
(T → C) ---------> (T → B)
|                  |
g' ∘ - |                  | g ∘ -
|                  |
∨                  ∨
(T → A) ---------> (T → X)
f ∘ -


is a pullback square for any type T.

## Definitions

### Postcomposition cones

postcomp-cone :
{l1 l2 l3 l4 l5 : Level}
{A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} (T : UU l5)
(f : A → X) (g : B → X) (c : cone f g C) →
cone (postcomp T f) (postcomp T g) (T → C)
pr1 (postcomp-cone T f g c) h = vertical-map-cone f g c ∘ h
pr1 (pr2 (postcomp-cone T f g c)) h = horizontal-map-cone f g c ∘ h
pr2 (pr2 (postcomp-cone T f g c)) h = eq-htpy (coherence-square-cone f g c ·r h)


## Properties

### The standard pullback of a postcomposition exponential computes as the type of cones

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

map-standard-pullback-postcomp :
standard-pullback (postcomp T f) (postcomp T g) → cone f g T
map-standard-pullback-postcomp = tot (λ _ → tot (λ _ → htpy-eq))

abstract
is-equiv-map-standard-pullback-postcomp :
is-equiv map-standard-pullback-postcomp
is-equiv-map-standard-pullback-postcomp =
is-equiv-tot-is-fiberwise-equiv
( λ p → is-equiv-tot-is-fiberwise-equiv (λ q → funext (f ∘ p) (g ∘ q)))

compute-standard-pullback-postcomp :
standard-pullback (postcomp T f) (postcomp T g) ≃ cone f g T
compute-standard-pullback-postcomp =
( map-standard-pullback-postcomp ,
is-equiv-map-standard-pullback-postcomp)


### The precomposition action on cones computes as the gap map of a postcomposition cone

triangle-map-standard-pullback-postcomp :
{l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
(T : UU l5) (f : A → X) (g : B → X) (c : cone f g C) →
coherence-triangle-maps
( cone-map f g c {T})
( map-standard-pullback-postcomp f g T)
( gap (postcomp T f) (postcomp T g) (postcomp-cone T f g c))
triangle-map-standard-pullback-postcomp T f g c h =
eq-pair-eq-fiber
( eq-pair-eq-fiber
( inv (is-section-eq-htpy (coherence-square-cone f g c ·r h))))


### Pullbacks are closed under postcomposition exponentiation

abstract
is-pullback-postcomp-is-pullback :
{l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
(f : A → X) (g : B → X) (c : cone f g C) → is-pullback f g c →
(T : UU l5) →
is-pullback (postcomp T f) (postcomp T g) (postcomp-cone T f g c)
is-pullback-postcomp-is-pullback f g c is-pb-c T =
is-equiv-top-map-triangle
( cone-map f g c)
( map-standard-pullback-postcomp f g T)
( gap (f ∘_) (g ∘_) (postcomp-cone T f g c))
( triangle-map-standard-pullback-postcomp T f g c)
( is-equiv-map-standard-pullback-postcomp f g T)
( universal-property-pullback-is-pullback f g c is-pb-c T)

abstract
is-pullback-is-pullback-postcomp :
{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) →
( {l5 : Level} (T : UU l5) →
is-pullback (postcomp T f) (postcomp T g) (postcomp-cone T f g c)) →
is-pullback f g c
is-pullback-is-pullback-postcomp f g c is-pb-postcomp =
is-pullback-universal-property-pullback f g c
( λ T →
is-equiv-left-map-triangle
( cone-map f g c)
( map-standard-pullback-postcomp f g T)
( gap (f ∘_) (g ∘_) (postcomp-cone T f g c))
( triangle-map-standard-pullback-postcomp T f g c)
( is-pb-postcomp T)
( is-equiv-map-standard-pullback-postcomp f g T))


### Cones satisfying the universal property of pullbacks are closed under postcomposition exponentiation

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

universal-property-pullback-postcomp-universal-property-pullback :
universal-property-pullback f g c →
universal-property-pullback
( postcomp T f)
( postcomp T g)
( postcomp-cone T f g c)
universal-property-pullback-postcomp-universal-property-pullback H =
universal-property-pullback-is-pullback
( postcomp T f)
( postcomp T g)
( postcomp-cone T f g c)
( is-pullback-postcomp-is-pullback f g c
( is-pullback-universal-property-pullback f g c H)
( T))


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