open import Cat.Prelude

module Cat.Diagram.Pullback { ℓ′} (C : Precategory  ℓ′) where


A pullback X×ZYX \times_Z Y of f:XZf : X \to Z and g:YZg : Y \to Z is the product of ff and gg in the category C/Z\ca{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

    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

    : {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 PP', 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
    {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