🔍

Equations Inline Footnotes

open import Cat.Functor.Adjoint.Comonadic
open import Cat.Functor.Equivalence.Path
open import Cat.Instances.Slice.Colimit
open import Cat.Instances.Slice.Limit
open import Cat.Instances.Slice.Twice
open import Cat.Diagram.Colimit.Base
open import Cat.Instances.Coalgebras
open import Cat.Functor.Equivalence
open import Cat.Diagram.Limit.Base
open import Cat.Functor.Properties
open import Cat.Diagram.Pullback
open import Cat.Diagram.Initial
open import Cat.Diagram.Product
open import Cat.Displayed.Total
open import Cat.Functor.Adjoint
open import Cat.Functor.Compose
open import Cat.Instances.Comma
open import Cat.Instances.Slice
open import Cat.Functor.Base
open import Cat.Connected
open import Cat.Univalent
open import Cat.Prelude

import Cat.Reasoning

open Coalgebra-on
open ∫Hom

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

open Cat.Reasoning C
open is-pullback
open Pullback
open Initial
open Functor
open _=>_
open /-Obj
open /-Hom

Base change🔗

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

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

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 .dom = 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{\times }_{X}K\to Y{\times }_X{K}^{\prime }\text{,}$ by observing that the square diagram below is a cone over $K^{\prime }\to X\leftarrow Y\text{.}$

  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 .com) ∙ xpb.square)
    dh' .com = ypb.p₂∘universal

  Base-change .F-id {x} = ext (xpb.unique id-comm (idr _))
    where module xpb = Pullback (pullbacks (x .map) f)

  Base-change .F-∘ {x} {y} {z} am bm =
    ext (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🔗

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 ; com = pullr (dh .com) }
  Σf .F-id    = ext refl
  Σf .F-∘ f g = ext refl

By the characterisation of iterated slices, we may identify $\mathcal{C}/Y$ with $(\mathcal{C}/B)/f\text{;}$ under this identification, the base change functor is identical to the “constant families” functor $f^{\ast }:\mathcal{C}/B\to (\mathcal{C}/B)/f$ (seeing $f$ as an object of $\mathcal{C}/B$ rather than a morphism of $\mathcal{C}\text{,}$ and remembering that products with $f$ in $\mathcal{C}/B$ are pullbacks along $f$ in $\mathcal{C}\text{),}$ while the left adjoint ${\Sigma }_f$ coincides with the forgetful functor $(\mathcal{C}/B)/f\to \mathcal{C}/B\text{.}$

Forget/≡Σf
  : {X Y : Ob} (f : Hom Y X)
  → PathP (λ i → Functor (Twice≡Slice {C = C} f i) (Slice C X))
    Forget/ (Σf f)
Forget/≡Σf f = Precategory-path→ _ _ $ Functor-path
  (λ o → /-Obj-path refl (sym (o .map .com)))
  λ f → /-Hom-pathp _ _ refl

Σ-iso-equiv
  : {X Y : Ob} {f : Hom Y X}
  → Cat.Reasoning.is-invertible C f
  → is-equivalence (Σf f)
Σ-iso-equiv {X} {f = f} isom = ff+split-eso→is-equivalence Σ-ff Σ-seso where
  module Sl = Cat.Reasoning (Slice C X)
  module isom = is-invertible isom

  func = Σf f
  Σ-ff : ∀ {x y} → is-equiv (func .F₁ {x} {y})
  Σ-ff = is-iso→is-equiv (iso ∘inv (λ x → ext refl) (λ x → ext refl)) where
    ∘inv : /-Hom _ _ → /-Hom _ _
    ∘inv o .map = o .map
    ∘inv o .com = invertible→monic isom _ _ (assoc _ _ _ ∙ o .com)

  Σ-seso : is-split-eso func
  Σ-seso y = cut (isom.inv ∘ y .map)
           , Sl.make-iso! into from' (eliml refl) (eliml refl)
    where
    into : /-Hom _ _
    into .map = id
    into .com = id-comm ∙ sym (pulll isom.invl)

    from' : /-Hom _ _
    from' .map = id
    from' .com = elimr refl ∙ cancell isom.invl

_ = Forget⊣constant-family
_ = Forget/-comonadic

module _ (pullbacks : ∀ {X Y Z} f g → Pullback C {X} {Y} {Z} f g) {X Y : Ob} (f : Hom Y X) where
  open _⊣_
  open _=>_

  private
    prod/ : has-products (Slice C X)
    prod/ = Slice-products pullbacks

  constant-family≡Base-change
    : PathP (λ i → Functor (Slice C X) (Twice≡Slice {C = C} f i))
      (constant-family prod/) (Base-change pullbacks f)
  constant-family≡Base-change = →Precategory-path _ _ $ Functor-path
    (λ o → /-Obj-path refl refl)
    λ g → /-Hom-pathp _ _ (ap (Pullback.universal (pullbacks _ _)) prop!)

Thus, many of the results in this section could in principle be derived automatically, but we opt to spell them out explicitly for formalisation reasons.

The unit and counit of the adjunction ${\Sigma }_f⊣f^{\ast }$ are given by the universal properties of pullbacks; this is an instance of the Forget⊣constant-family adjunction.

  Σ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 .com = 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 .com)))
    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 .com = 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)

This adjunction is comonadic. This generalises the fact that the forgetful functor $\mathcal{C}/Y\to \mathcal{C}$ is comonadic, which we recover by taking $f:Y\to \top \text{;}$ by the discussion above, it is also a consequence of the same fact applied to the forgetful functor $(\mathcal{C}/B)/f\to \mathcal{C}/B\text{.}$

The idea is the same, only with more dependent types: thinking of $Y$ as a family of types over $X\text{,}$ the comonad ${\Sigma }_f\circ f^{\ast }:\mathcal{C}/X\to \mathcal{C}/X$ sends a map $A\to X$ to the projection map $A{\times }_{X}Y\to X\text{.}$ Therefore, a coalgebra for this comonad consists of a map $⟨g,h⟩:A\to A{\times }_{X}Y$ over $X\text{;}$ but the coalgebra laws force $g$ to be the identity on $A\text{,}$ so all that is left is the map $h\text{,}$ an object of $(\mathcal{C}/X)/f\text{,}$ or in other words $\mathcal{C}/Y\text{.}$

  Σf-comonadic : is-comonadic Σf⊣f*
  Σf-comonadic = is-precat-iso→is-equivalence
    (iso (is-iso→is-equiv ff) (is-iso→is-equiv eso))
    where
      open is-iso

      eso : is-iso (Comparison-CoEM Σf⊣f* .F₀)
      eso .from (A , c) = cut (pb.p₂ ∘ c .ρ .map)
        where module pb = Pullback (pullbacks (A .map) f)
      eso .rinv (A , c) =
          Σ-pathp (/-Obj-path refl path)
        $ Coalgebra-on-pathp _ $ /-Hom-pathp _ _
        $ symP $ Hom-pathp-reflr C $ sym $ pb≡.unique i0
          (pulll (from-pathp-to' C _ λ i → pb≡.p₁ i) ∙ unext (c .ρ-counit))
          (pulll (from-pathp-to' C _ λ i → pb≡.p₂ i))
        where
          module pb = Pullback (pullbacks (A .map) f)

          path : f ∘ pb.p₂ ∘ c .ρ .map ≡ A .map
          path = assoc _ _ _ ∙ unext (c .ρ .com)

          module pb≡ i = Pullback (pullbacks (path i) f)
      eso .linv p = /-Obj-path refl pb.p₂∘universal
        where module pb = Pullback (pullbacks (f ∘ p .map) f)

      ff : ∀ {x y} → is-iso (Comparison-CoEM Σf⊣f* .F₁ {x} {y})
      ff .from g .map = g .fst .map
      ff {x} {y} .from g .com =
        y .map ∘ g .fst .map                       ≡˘⟨ pulll pby.p₂∘universal ⟩≡˘
        pby.p₂ ∘ pby.universal _ ∘ g .fst .map     ≡˘⟨ refl⟩∘⟨ unext (g .snd) ⟩≡˘
        pby.p₂ ∘ pby.universal _ ∘ pbx.universal _ ≡⟨ pulll pby.p₂∘universal ⟩≡
        pbx.p₂ ∘ pbx.universal _                   ≡⟨ pbx.p₂∘universal ⟩≡
        x .map                                     ∎
        where
          module pbx = Pullback (pullbacks (f ∘ x .map) f)
          module pby = Pullback (pullbacks (f ∘ y .map) f)
      ff .rinv _ = ext refl
      ff .linv _ = ext refl

By transporting the analogous results for Forget/, ${\Sigma }_f$ creates connected limits and all colimits.

module _ {oj ℓj} {J : Precategory oj ℓj} {X Y} {f : Hom X Y} where

  Σf-creates-connected-limits
    : is-connected-cat J
    → creates-limits-of J (Σf f)
  Σf-creates-connected-limits conn = substd (creates-limits-of J)
    (Forget/≡Σf f) (Forget/-creates-connected-limits conn)

  Σf-creates-colimits : creates-colimits-of J (Σf f)
  Σf-creates-colimits = substd (creates-colimits-of J)
    (Forget/≡Σf f) Forget/-creates-colimits

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)