module Cat.Functor.Pullback
  {o β„“} {C : Precategory o β„“}
  where

Base changeπŸ”—

Let be a category with all pullbacks, and a morphism in Then we have a functor called the base change, where the action on objects is given by pulling back along

On objects, the functor maps as in the diagram below. It’s a bit busy, so look at it in parts: On the left we have the object of and on the right we have the whole pullback diagram, showing how the parts fit together. The actual object of the functor gives is the vertical arrow

module _ (pullbacks : βˆ€ {X Y Z} f g β†’ Pullback C {X} {Y} {Z} f g) {X Y : Ob} (f : Hom Y X) where
  Base-change : Functor (Slice C X) (Slice C Y)
  Base-change .Fβ‚€ x = ob where
    ob : /-Obj Y
    ob .domain = pullbacks (x .map) f .apex
    ob .map    = pullbacks (x .map) f .pβ‚‚

On morphisms, we use the universal property of the pullback to obtain a map by observing that the square diagram below is a cone over

  Base-change .F₁ {x} {y} dh = dh' where
    module ypb = Pullback (pullbacks (y .map) f)
    module xpb = Pullback (pullbacks (x .map) f)
    dh' : /-Hom _ _
    dh' .map = ypb.universal {p₁' = dh .map ∘ xpb.p₁}
      (pulll (dh .commutes) βˆ™ xpb.square)
    dh' .commutes = ypb.pβ‚‚βˆ˜universal
The properties of pullbacks also guarantee that this operation is functorial, but the details are not particularly enlightening.
  Base-change .F-id {x} = ext (sym (xpb.unique id-comm (idr _)))
    where module xpb = Pullback (pullbacks (x .map) f)

  Base-change .F-∘ {x} {y} {z} am bm =
    ext (sym (zpb.unique
      (pulll zpb.pβ‚βˆ˜universal βˆ™ pullr ypb.pβ‚βˆ˜universal βˆ™ assoc _ _ _)
      (pulll zpb.pβ‚‚βˆ˜universal βˆ™ ypb.pβ‚‚βˆ˜universal)))
    where
      module ypb = Pullback (pullbacks (y .map) f)
      module zpb = Pullback (pullbacks (z .map) f)

PropertiesπŸ”—

The base change functor is a right adjoint. We construct the left adjoint directly, then give the unit and counit, and finally prove the triangle identities.

The left adjoint, called dependent sum and written is given on objects by precomposition with and on morphisms by what is essentially the identity function β€” only the witness of commutativity must change.

module _ {X Y : Ob} (f : Hom Y X) where
  Ξ£f : Functor (Slice C Y) (Slice C X)
  Ξ£f .Fβ‚€ o = cut (f ∘ o .map)
  Ξ£f .F₁ dh = record { map = dh .map ; commutes = pullr (dh .commutes) }
  Ξ£f .F-id = trivial!
  Σf .F-∘ f g = trivial!

  open _⊣_

The adjunction unit and counit are given by the universal properties of pullbacks. ⚠️ WIP ⚠️

module _ (pullbacks : βˆ€ {X Y Z} f g β†’ Pullback C {X} {Y} {Z} f g) {X Y : Ob} (f : Hom Y X) where
  open _⊣_
  open _=>_

  Σf⊣f* : Σf f ⊣ Base-change pullbacks f
  Σf⊣f* .unit .η obj = dh where
    module pb = Pullback (pullbacks (f ∘ obj .map) f)
    dh : /-Hom _ _
    dh .map = pb.universal {p₁' = id} {pβ‚‚' = obj .map} (idr _)
    dh .commutes = pb.pβ‚‚βˆ˜universal
  Σf⊣f* .unit .is-natural x y g =
    ext (pb.uniqueβ‚‚
      {p = (f ∘ y .map) ∘ id ∘ g .map β‰‘βŸ¨ cat! C βŸ©β‰‘ f ∘ y .map ∘ g .map ∎}
      (pulll pb.pβ‚βˆ˜universal)
      (pulll pb.pβ‚‚βˆ˜universal)
      (pulll pb.pβ‚βˆ˜universal βˆ™ pullr pb'.pβ‚βˆ˜universal βˆ™ id-comm)
      (pulll pb.pβ‚‚βˆ˜universal βˆ™ pb'.pβ‚‚βˆ˜universal βˆ™ sym (g .commutes)))
    where
      module pb = Pullback (pullbacks (f ∘ y .map) f)
      module pb' = Pullback (pullbacks (f ∘ x .map) f)

  Σf⊣f* .counit .η obj = dh where
    module pb = Pullback (pullbacks (obj .map) f)
    dh : /-Hom _ _
    dh .map = pb.p₁
    dh .commutes = pb.square
  Ξ£f⊣f* .counit .is-natural x y g = ext pb.pβ‚βˆ˜universal
    where module pb = Pullback (pullbacks (y .map) f)

  Ξ£f⊣f* .zig {A} = ext pb.pβ‚βˆ˜universal
    where module pb = Pullback (pullbacks (f ∘ A .map) f)

  Σf⊣f* .zag {B} = ext
    (sym (pb.uniqueβ‚‚ {p = pb.square}
      (idr _) (idr _)
      (pulll pb.pβ‚βˆ˜universal βˆ™ pullr pb'.pβ‚βˆ˜universal βˆ™ idr _)
      (pulll pb.pβ‚‚βˆ˜universal βˆ™ pb'.pβ‚‚βˆ˜universal))) where
    module pb = Pullback (pullbacks (B .map) f)
    module pb' = Pullback (pullbacks (f ∘ pb.pβ‚‚) f)

Equifibred natural transformationsπŸ”—

A natural transformation is called equifibred, or cartesian, if each of its naturality squares is a pullback:

is-equifibred
  : βˆ€ {oj β„“j} {J : Precategory oj β„“j} {F G : Functor J C}
  β†’ F => G β†’ Type _
is-equifibred {J = J} {F} {G} Ξ± =
  βˆ€ {x y} (f : J .Precategory.Hom x y)
  β†’ is-pullback C (F .F₁ f) (Ξ± .Ξ· y) (Ξ± .Ξ· x) (G .F₁ f)

An easy property of equifibered transformations is that they are closed under pre-whiskering:

β—‚-equifibred
  : βˆ€ {oj β„“j ok β„“k} {J : Precategory oj β„“j} {K : Precategory ok β„“k}
  β†’ {F G : Functor J C} (H : Functor K J) (Ξ± : F => G)
  β†’ is-equifibred Ξ± β†’ is-equifibred (Ξ± β—‚ H)
β—‚-equifibred H Ξ± eq f = eq (H .F₁ f)