open import Cat.Prelude

module Cat.Diagram.Pullback {β„“ β„“β€²} (C : Precategory β„“ β„“β€²) where

PullbacksπŸ”—

A pullback X×ZYX \times_Z Y of f:X→Zf : X \to Z and g:Y→Zg : Y \to Z is the product of ff and gg in the category C/Z\mathcal{C}/Z, the category of objects fibred over ZZ. We note that the fibre of X×ZYX \times_Z Y over some element xx of ZZ is the product of the fibres of ff and gg over xx; Hence the pullback is also called the fibred product.

record is-pullback {P} (p₁ : Hom P X) (f : Hom X Z) (pβ‚‚ : Hom P Y) (g : Hom Y Z)
  : Type (β„“ βŠ” β„“β€²) where

  no-eta-equality
  field
    square   : f ∘ p₁ ≑ g ∘ pβ‚‚

The concrete incarnation of the abstract nonsense above is that a pullback turns out to be a universal square like the one below. Since it is a product, it comes equipped with projections Ο€1\pi_1 and Ο€2\pi_2 onto its factors; Since isn’t merely a product of XX and YY, but rather of XX and YY considered as objects over ZZ in a specified way, overall square has to commute.

    limiting : βˆ€ {Pβ€²} {p₁' : Hom Pβ€² X} {pβ‚‚' : Hom Pβ€² Y}
             β†’ f ∘ p₁' ≑ g ∘ pβ‚‚' β†’ Hom Pβ€² P
    pβ‚βˆ˜limiting : {p : f ∘ p₁' ≑ g ∘ pβ‚‚'} β†’ p₁ ∘ limiting p ≑ p₁'
    pβ‚‚βˆ˜limiting : {p : f ∘ p₁' ≑ g ∘ pβ‚‚'} β†’ pβ‚‚ ∘ limiting p ≑ pβ‚‚'

    unique : {p : f ∘ p₁' ≑ g ∘ pβ‚‚'} {lim' : Hom Pβ€² P}
           β†’ p₁ ∘ lim' ≑ p₁'
           β†’ pβ‚‚ ∘ lim' ≑ pβ‚‚'
           β†’ lim' ≑ limiting p

  uniqueβ‚‚
    : {p : f ∘ p₁' ≑ g ∘ pβ‚‚'} {lim' lim'' : Hom Pβ€² P}
    β†’ p₁ ∘ lim' ≑ p₁' β†’ pβ‚‚ ∘ lim' ≑ pβ‚‚'
    β†’ p₁ ∘ lim'' ≑ p₁' β†’ pβ‚‚ ∘ lim'' ≑ pβ‚‚'
    β†’ lim' ≑ lim''
  uniqueβ‚‚ {p = o} p q r s = unique {p = o} p q βˆ™ sym (unique r s)

By universal, we mean that any other β€œsquare” (here the second β€œsquare” has corners Pβ€²P', XX, YY, ZZ β€” it’s a bit bent) admits a unique factorisation that passes through PP; We can draw the whole situation as in the diagram below. Note the little corner on PP, indicating that the square is a pullback.

We provide a convenient packaging of the pullback and the projection maps:

record Pullback {X Y Z} (f : Hom X Z) (g : Hom Y Z) : Type (β„“ βŠ” β„“β€²) where
  no-eta-equality
  field
    {apex} : Ob
    p₁ : Hom apex X
    pβ‚‚ : Hom apex Y
    has-is-pb : is-pullback p₁ f pβ‚‚ g

  open is-pullback has-is-pb public