open import Cat.Functor.Equivalence
open import Cat.Diagram.Pullback
open import Cat.Diagram.Initial
open import Cat.Functor.Adjoint
open import Cat.Instances.Comma
open import Cat.Instances.Slice
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Reasoning

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

Base changeπŸ”—

Let C\ca{C} be a category with all pullbacks, and f:Yβ†’Xf : Y \to X a morphism in C\ca{C}. Then we have a functor fβˆ—:C/Xβ†’C/Yf* : \ca{C}/X \to \ca{C}/Y, called the base change, where the action on objects is given by pulling back along ff.

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β†’gXK \xto{g} X of C/X\ca{C}/X, and on the right we have the whole pullback diagram, showing how the parts fit together. The actual object of C/Y\ca{C}/Y the functor gives is the vertical arrow YΓ—XKβ†’YY \times_X K \to Y.

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 YΓ—XKβ†’YΓ—XKβ€²Y \times_X K \to Y \times_X K', by observing that the square diagram below is a cone over Kβ€²β†’X←YK' \to X \ot Y.

  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.limiting {p₁' = dh .map ∘ xpb.p₁}
      (pulll (dh .commutes) βˆ™ xpb.square)
    dhβ€² .commutes = ypb.pβ‚‚βˆ˜limiting
The properties of pullbacks also guarantee that this operation is functorial, but the details are not particularly enlightening.
  Base-change .F-id {x} = /-Hom-path (sym (xpb.unique id-comm (idr _)))
    where module xpb = Pullback (pullbacks (x .map) f)

  Base-change .F-∘ {x} {y} {z} am bm =
    /-Hom-path (sym (zpb.unique
      (pulll zpb.pβ‚βˆ˜limiting βˆ™ pullr ypb.pβ‚βˆ˜limiting βˆ™ assoc _ _ _)
      (pulll zpb.pβ‚‚βˆ˜limiting βˆ™ ypb.pβ‚‚βˆ˜limiting)))
    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 βˆ‘f\sum_f, is given on objects by precomposition with ff, 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 = /-Hom-path refl
  Σf .F-∘ f g = /-Hom-path refl

  open _⊣_
  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.limiting {p₁' = id} {pβ‚‚' = obj .map} (idr _)
    dh .commutes = pb.pβ‚‚βˆ˜limiting
  Σf⊣f* .unit .is-natural x y g =
    /-Hom-path (pb.uniqueβ‚‚
      {p = (f ∘ y .map) ∘ id ∘ g .map β‰‘βŸ¨ solve C βŸ©β‰‘ f ∘ y .map ∘ g .map ∎}
      (pulll pb.pβ‚βˆ˜limiting)
      (pulll pb.pβ‚‚βˆ˜limiting)
      (pulll pb.pβ‚βˆ˜limiting βˆ™ pullr pbβ€².pβ‚βˆ˜limiting βˆ™ id-comm)
      (pulll pb.pβ‚‚βˆ˜limiting βˆ™ pbβ€².pβ‚‚βˆ˜limiting βˆ™ 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 = /-Hom-path pb.pβ‚βˆ˜limiting
    where module pb = Pullback (pullbacks (y .map) f)

  Ξ£f⊣f* .zig {A} = /-Hom-path pb.pβ‚βˆ˜limiting
    where module pb = Pullback (pullbacks (f ∘ A .map) f)

  Σf⊣f* .zag {B} = /-Hom-path
    (sym (pb.uniqueβ‚‚ {p = pb.square}
      (idr _) (idr _)
      (pulll pb.pβ‚βˆ˜limiting βˆ™ pullr pbβ€².pβ‚βˆ˜limiting βˆ™ idr _)
      (pulll pb.pβ‚‚βˆ˜limiting βˆ™ pbβ€².pβ‚‚βˆ˜limiting))) where
    module pb = Pullback (pullbacks (B .map) f)
    module pbβ€² = Pullback (pullbacks (f ∘ pb.pβ‚‚) f)