open import Cat.Prelude

import Cat.Reasoning

module Cat.Diagram.Pullback where

PullbacksπŸ”—

module _ {o β„“} (C : Precategory o β„“) where
  open Cat.Reasoning C
  private variable
    P' X Y Z : Ob
    h p₁' pβ‚‚' : Hom X Y

A pullback of and is the product of and in the category the category of objects fibred over We note that the fibre of over some element of is the product of the fibres of and over 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 (o βŠ” β„“) 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 and onto its factors; Since isn’t merely a product of and but rather of and considered as objects over 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 β€” it’s a bit bent) admits a unique factorisation that passes through We can draw the whole situation as in the diagram below. Note the little corner on 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 (o βŠ” β„“) 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 : βˆ€ {o β„“} β†’ Precategory o β„“ β†’ Type _
has-pullbacks C = βˆ€ {A B X} (f : Hom A X) (g : Hom B X) β†’ Pullback C f g
  where open Precategory C

module Pullbacks
  {o β„“}
  (C : Precategory o β„“)
  (all-pullbacks : has-pullbacks  C)
  where
  open Precategory C
  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 as encoding the data of a family over (think of the special case where and then we can think of pulling back along as β€œthe universal solution to making a family over via ”. 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 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.

module _ {o β„“} (C : Precategory o β„“) where
  open Cat.Reasoning C

  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 C f⁺ g p2 f β†’ P f⁺