# The universal property of pullbacks

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Victor Blanchi.

Created on 2022-02-10.

module foundation.universal-property-pullbacks where

open import foundation-core.universal-property-pullbacks public

Imports
open import foundation.cones-over-cospan-diagrams
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.subtype-identity-principle
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.function-types
open import foundation-core.pullbacks


## Idea

The universal property of pullbacks describes the optimal way to complete a diagram of the form

           B
|
|
∨
A -----> X


to a square

  C -----> B
| ⌟      |
|        |
∨        ∨
A -----> X.


## Properties

### Unique uniqueness of pullbacks

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

abstract
uniquely-unique-universal-property-pullback :
( c' : cone f g C') (c : cone f g C) →
( up-c' : universal-property-pullback f g c') →
( up-c : universal-property-pullback f g c) →
is-contr
( Σ (C' ≃ C) (λ e → htpy-cone f g (cone-map f g c (map-equiv e)) c'))
uniquely-unique-universal-property-pullback c' c up-c' up-c =
is-torsorial-Eq-subtype
( uniqueness-universal-property-pullback f g c up-c C' c')
( is-property-is-equiv)
( map-universal-property-pullback f g c up-c c')
( htpy-cone-map-universal-property-pullback f g c up-c c')
( is-equiv-up-pullback-up-pullback c c'
( map-universal-property-pullback f g c up-c c')
( htpy-cone-map-universal-property-pullback f g c up-c c')
up-c up-c')


### The horizontal pullback pasting property

Given a diagram

  ∙ -------> ∙ -------> ∙
|          | ⌟        |
|          |          |
∨          ∨          ∨
∙ -------> ∙ -------> ∙


where the right-hand square is a pullback, then the left-hand square is a pullback if and only if the composite square is.

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

abstract
universal-property-pullback-rectangle-universal-property-pullback-left-square :
(c : cone j h B) (d : cone i (vertical-map-cone j h c) A) →
universal-property-pullback j h c →
universal-property-pullback i (vertical-map-cone j h c) d →
universal-property-pullback (j ∘ i) h (pasting-horizontal-cone i j h c d)
universal-property-pullback-rectangle-universal-property-pullback-left-square
c d up-pb-c up-pb-d =
universal-property-pullback-is-pullback (j ∘ i) h
( pasting-horizontal-cone i j h c d)
( is-pullback-rectangle-is-pullback-left-square i j h c d
( is-pullback-universal-property-pullback j h c up-pb-c)
( is-pullback-universal-property-pullback i
( vertical-map-cone j h c) d up-pb-d))

abstract
universal-property-pullback-left-square-universal-property-pullback-rectangle :
(c : cone j h B) (d : cone i (vertical-map-cone j h c) A) →
universal-property-pullback j h c →
universal-property-pullback (j ∘ i) h
( pasting-horizontal-cone i j h c d) →
universal-property-pullback i (vertical-map-cone j h c) d
universal-property-pullback-left-square-universal-property-pullback-rectangle
c d up-pb-c up-pb-rect =
universal-property-pullback-is-pullback
( i)
( vertical-map-cone j h c)
( d)
( is-pullback-left-square-is-pullback-rectangle i j h c d
( is-pullback-universal-property-pullback j h c up-pb-c)
( is-pullback-universal-property-pullback (j ∘ i) h
( pasting-horizontal-cone i j h c d) up-pb-rect))


### The vertical pullback pasting property

Given a diagram

  ∙ -------> ∙
|          |
|          |
∨          ∨
∙ -------> ∙
| ⌟        |
|          |
∨          ∨
∙ -------> ∙


where the bottom square is a pullback, then the top square is a pullback if and only if the composite square is.

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

abstract
universal-property-pullback-top-universal-property-pullback-rectangle :
(c : cone f g B) (d : cone (horizontal-map-cone f g c) h A) →
universal-property-pullback f g c →
universal-property-pullback f (g ∘ h) (pasting-vertical-cone f g h c d) →
universal-property-pullback (horizontal-map-cone f g c) h d
universal-property-pullback-top-universal-property-pullback-rectangle
c d up-pb-c up-pb-dc =
universal-property-pullback-is-pullback
( horizontal-map-cone f g c)
( h)
( d)
( is-pullback-top-square-is-pullback-rectangle f g h c d
( is-pullback-universal-property-pullback f g c up-pb-c)
( is-pullback-universal-property-pullback f (g ∘ h)
( pasting-vertical-cone f g h c d)
( up-pb-dc)))

abstract
universal-property-pullback-rectangle-universal-property-pullback-top :
(c : cone f g B) (d : cone (horizontal-map-cone f g c) h A) →
universal-property-pullback f g c →
universal-property-pullback (horizontal-map-cone f g c) h d →
universal-property-pullback f (g ∘ h) (pasting-vertical-cone f g h c d)
universal-property-pullback-rectangle-universal-property-pullback-top
c d up-pb-c up-pb-d =
universal-property-pullback-is-pullback
( f)
( g ∘ h)
( pasting-vertical-cone f g h c d)
( is-pullback-rectangle-is-pullback-top-square f g h c d
( is-pullback-universal-property-pullback f g c up-pb-c)
( is-pullback-universal-property-pullback
( horizontal-map-cone f g c)
( h)
( d)
( up-pb-d)))


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