open import Cat.Prelude

import Cat.Reasoning

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

PullbacksπŸ”—

open Cat.Reasoning C
private variable
  P' X Y Z : Ob
  h p₁' pβ‚‚' : Hom X Y

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.

    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)

  pullback-univ
    : βˆ€ {O} β†’ Hom O P ≃ (Ξ£ (Hom O X) Ξ» h β†’ Ξ£ (Hom O Y) Ξ» h' β†’ f ∘ h ≑ g ∘ h')
  pullback-univ .fst h = p₁ ∘ h , pβ‚‚ ∘ h , extendl square
  pullback-univ .snd = is-iso→is-equiv λ where
    .is-iso.inv (f , g , Ξ±) β†’ universal Ξ±
    .is-iso.rinv x β†’ Ξ£-pathp pβ‚βˆ˜universal $ Ξ£-prop-pathp (Ξ» _ _ β†’ hlevel 1) pβ‚‚βˆ˜universal
    .is-iso.linv x β†’ sym (unique refl refl)

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

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β†’Bf : A \to B as encoding the data of a family over BB (think of the special case where A=Ξ£x:AF(x)A = \Sigma_{x : A} F(x), and f=Ο€1f = \pi_1), then we can think of pulling back ff along g:Xβ†’Bg : X \to B as β€œthe universal solution to making ff a family over XX, via gg”. 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 ff 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⁺