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
$\mathcal{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 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 $\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.

universal : β {Pβ²} {pβ' : Hom Pβ² X} {pβ' : Hom Pβ² Y} β f β pβ' β‘ g β pβ' β Hom Pβ² P pββuniversal : {p : f β pβ' β‘ g β pβ'} β pβ β universal p β‘ pβ' pββuniversal : {p : f β pβ' β‘ g β pβ'} β pβ β universal p β‘ pβ' unique : {p : f β pβ' β‘ g β pβ'} {lim' : Hom Pβ² P} β pβ β lim' β‘ pβ' β pβ β lim' β‘ pβ' β lim' β‘ universal 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 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

# Categories with all pullbacksπ

We also provide a helper module for working with categories that have all pullbacks.

has-pullbacks : Type _ has-pullbacks = β {A B X} (f : Hom A X) (g : Hom B X) β Pullback f g module Pullbacks (all-pullbacks : has-pullbacks) where module pullback {x y z} (f : Hom x z) (g : Hom y z) = Pullback (all-pullbacks f g) Pb : β {x y z} β Hom x z β Hom y z β Ob Pb = pullback.apex

## Stabilityπ

Pullbacks, in addition to their nature as limits, serve as the way of βchanging the baseβ of a family of objects: if we think of an arrow $f : A \to B$ as encoding the data of a family over $B$ (think of the special case where $A = \Sigma_{x : A} F(x)$, and $f = \pi_1$), then we can think of pulling back $f$ along $g : X \to B$ as βthe universal solution to making $f$ a family over $X$, via $g$β. One way of making this intuition formal is through the fundamental fibration of a category with pullbacks.

In that framing, there is a canonical choice for βtheβ pullback of an
arrow along another: We put the arrow
$f$
we want to pullback on the right side of the diagram, and the pullback
is the right arrow. Using the type is-pullback defined above, the arrow which
results from pulling back is adjacent **to the
adjustment**: `is-pullback fβΊ g _ f`

. To help keep
this straight, we define what it means for a class of arrows to be
**stable under pullback**: If `f`

has a given
property, then so does `fβΊ`

, for any pullback of
`f`

.

is-pullback-stable : β {ββ²} β (β {a b} β Hom a b β Type ββ²) β Type _ is-pullback-stable P = β {p A B X} (f : Hom A B) (g : Hom X B) {fβΊ : Hom p X} {p2} β P f β is-pullback fβΊ g p2 f β P fβΊ