open import Cat.Prelude

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

Pullbacks🔗

A pullback $X \times_Z Y$ of $f : X \to Z$ and $g : Y \to Z$ is the product of $f$ and $g$ in the category $\ca{C}/Z$, the category of objects fibred over $Z$. We note that the fibre of $X \times_Z Y$ over some element $x$ of $Z$ is the product of the fibres of $f$ and $g$ over $x$; 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

  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 $\pi_1$ and $\pi_2$ onto its factors; Since isn’t merely a product of $X$ and $Y$, but rather of $X$ and $Y$ considered as objects over $Z$ 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'$, $X$, $Y$, $Z$ — it’s a bit bent) admits a unique factorisation that passes through $P$; We can draw the whole situation as in the diagram below. Note the little corner on $P$, 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
  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