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