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

module _ {o β} {C : Precategory o β} where
open Cat.Reasoning C
private variable
P' X Y Z : Ob
h pβ' pβ' : Hom X Y

is-pullback-is-prop : β {P} {pβ : Hom P X} {f : Hom X Z} {pβ : Hom P Y} {g : Hom Y Z} β is-prop (is-pullback C pβ f pβ g)
is-pullback-is-prop {X = X} {Y = Y} {pβ = pβ} {f} {pβ} {g} x y = q where
open is-pullback
p : Path (β {P'} {pβ' : Hom P' X} {pβ' : Hom P' Y} β f β pβ' β‘ g β pβ' β _) (x .universal) (y .universal)
p i sq = y .unique {p = sq} (x .pββuniversal {p = sq}) (x .pββuniversal) i
q : x β‘ y
q i .square = Hom-set _ _ _ _ (x .square) (y .square) i
q i .universal = p i
q i .pββuniversal {pβ' = pβ'} {p = sq} = is-propβpathp (Ξ» i β Hom-set _ _ (pβ β p i sq) pβ') (x .pββuniversal) (y .pββuniversal) i
q i .pββuniversal {p = sq} = is-propβpathp (Ξ» i β Hom-set _ _ (pβ β p i sq) _) (x .pββuniversal) (y .pββuniversal) i
q i .unique {p = sq} {lim' = lim'} cβ cβ = is-propβpathp (Ξ» i β Hom-set _ _ lim' (p i sq)) (x .unique cβ cβ) (y .unique cβ cβ) i

instance
H-Level-is-pullback : β {P} {pβ : Hom P X} {f : Hom X Z} {pβ : Hom P Y} {g : Hom Y Z} {n} β H-Level (is-pullback C pβ f pβ g) (suc n)
H-Level-is-pullback = prop-instance is-pullback-is-prop


# 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 left 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βΊ