module Cat.Functor.Pullback
  {o ℓ} {C : Precategory o ℓ}
  where

Base change🔗

Let $C$ be a category with all pullbacks, and $f : Y \to X$ a morphism in $C .$ Then we have a functor $f^{*} : C / X \to C / Y,$ called the base change, where the action on objects is given by pulling back along $f .$

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 $K g X$ of $C / X,$ and on the right we have the whole pullback diagram, showing how the parts fit together. The actual object of $C / Y$ the functor gives is the vertical arrow $Y \times_{X} K \to Y .$

module _ (pullbacks : Pullbacks C) {X Y : Ob} (f : Hom Y X) where
  open Pullbacks pullbacks

  Base-change : Functor (Slice C X) (Slice C Y)
  Base-change .F₀ x = ob where
    ob : /-Obj Y
    ob .domain = Pb (x .map) f
    ob .map    = p₂ (x .map) f

On morphisms, we use the universal property of the pullback to obtain a map $Y \times_{X} K \to Y \times_{X} K^{'},$ by observing that the square diagram below is a cone over $K^{'} \to X \leftarrow Y .$

  Base-change .F₁ {x} {y} dh = dh' where
    dh' : /-Hom _ _
    dh' .map = pb (dh .map ∘ p₁ (x .map) f) _ (pulll (dh .commutes) ∙ square)
    dh' .commutes = p₂∘pb

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 (pb-unique id-comm (idr _)))

  Base-change .F-∘ {x} {y} {z} am bm =
    ext (sym (pb-unique
      (pulll p₁∘pb ∙ pullr p₁∘pb ∙ assoc _ _ _)
      (pulll p₂∘pb ∙ p₂∘pb)))

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 $\sum_{f},$ is given on objects by precomposition with $f,$ 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 : Pullbacks C) {X Y : Ob} (f : Hom Y X) where
  open Pullbacks pullbacks
  open _⊣_
  open _=>_

  Σf⊣f* : Σf f ⊣ Base-change pullbacks f
  Σf⊣f* .unit .η obj = dh where
    dh : /-Hom _ _
    dh .map = pb id (obj .map) (idr _)
    dh .commutes = p₂∘pb
  Σ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 p₁∘pb)
      (pulll p₂∘pb)
      (pulll p₁∘pb ∙ pullr p₁∘pb ∙ id-comm)
      (pulll p₂∘pb ∙ p₂∘pb ∙ sym (g .commutes)))

  Σf⊣f* .counit .η obj = dh where
    dh : /-Hom _ _
    dh .map = p₁ (obj .map) f
    dh .commutes = square
  Σf⊣f* .counit .is-natural x y g = ext p₁∘pb
  Σf⊣f* .zig {A} = ext p₁∘pb
  Σf⊣f* .zag {B} = ext
    (sym (pb-unique₂ {p = square}
      (idr _) (idr _)
      (pulll p₁∘pb ∙ pullr p₁∘pb ∙ idr _)
      (pulll p₂∘pb ∙ p₂∘pb)))

Equifibred natural transformations🔗

A natural transformation $F \Rightarrow G$ 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)